5 papers
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
Gabriele Masina, Emanuele Civini, Massimo Michelutti +2
In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or…
Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
Emanuele Civini, Gabriele Masina, Giuseppe Spallitta +1
Lifting Boolean-reasoning techniques to the SMT level most often requires producing theory lemmas that rule out theory-inconsistent truth assignments. With standard SMT solving, it…
Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Roberto Sebastiani
Many procedures for SAT-related problems, in particular for those requiring the complete enumeration of satisfying truth assignments, rely their efficiency and effectiveness on the…
Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
Gabriele Masina, Roberto Sebastiani
Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) with the task of optimizing some objective function(s). In OMT solvers, a CDCL-based SMT solver enum…
Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
All-Solution Satisfiability (AllSAT) and its extension, All-Solution Satisfiability Modulo Theories (AllSMT), have become more relevant in recent years, mainly in formal verificati…