research
∙
06/01/2023
Enumerating Disjoint Partial Models without Blocking Clauses
A basic algorithm for enumerating disjoint propositional models (disjoin...
share
research
∙
03/27/2023
On CNF Conversion for SAT Enumeration
Modern SAT solvers are designed to handle problems expressed in Conjunct...
research
∙
02/13/2023
Enhancing SMT-based Weighted Model Integration by Structure Awareness
The development of efficient exact and approximate algorithms for probab...
research
∙
06/28/2022
SMT-based Weighted Model Integration with Structure Awareness
Weighted Model Integration (WMI) is a popular formalism aimed at unifyin...
research
∙
10/22/2021
On Enumerating Short Projected Models
Propositional model enumeration, or All-SAT, is the task to record all m...
research
∙
02/28/2020
Are You Satisfied by This Partial Assignment?
Many procedures for SAT and SAT-related problems – in particular for tho...
research
∙
12/03/2019
From MiniZinc to Optimization Modulo Theories, and Back (Extended Version)
Optimization Modulo Theories (OMT) is an extension of SMT that allows fo...
research
∙
05/07/2019
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers
Optimization Modulo Theories (OMT) is an important extension of SMT whic...
research
∙
03/05/2018
OpenMath and SMT-LIB
OpenMath and SMT-LIB are languages with very different origins, but both...
research
∙
01/26/2018
Satisfiability Modulo Transcendental Functions via Incremental Linearization
In this paper we present an abstraction-refinement approach to Satisfiab...
research
∙
01/26/2018
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Model checking invariant properties of designs, represented as transitio...
research
∙
01/27/2016
Multi-Object Reasoning with Constrained Goal Models
Goal models have been widely used in Computer Science to represent softw...
research
∙
05/07/2014
Structured Learning Modulo Theories
Modelling problems containing a mixture of Boolean and numerical variabl...
research
∙
02/18/2014
Hybrid SRL with Optimization Modulo Theories
Generally speaking, the goal of constructive learning could be seen as, ...
research
∙
01/16/2014
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
The problem of finding small unsatisfiable cores for SAT formulas has re...
research
∙
01/15/2014
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
In the last two decades, modal and description logics have been applied ...
research
∙
02/07/2012