1 citations · 1 across the 4 of their papers we have counts for
6 papers
Computing Short SAT Implicants via Ising/QUBO Encodings
Giuseppe Spallitta, Leonardo Duenas-Osorio, Moshe Y. Vardi
Many reasoning tasks require short partial satisfying assignments (implicants), sometimes focusing on a set of important variables. SAT-to-Ising-QUBO formulations are implicitly de…
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…
Extending CDCL-based Model Enumeration with Weights
Giuseppe Spallitta, Moshe Y. Vardi
In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for t…
On CNF Conversion for SAT and SMT Enumeration
Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
Modern SAT and SMT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants…
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…