1 citations · 1 across the 5 of their papers we have counts for
8 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…
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…
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…
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…
Experimenting with D-Wave Quantum Annealers on Prime Factorization problems
Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
This paper builds on top of a paper we have published very recently, in which we have proposed a novel approach to prime factorization (PF) by quantum annealing, where 8,219,999=32…