8 citations · 31 across the 12 of their papers we have counts for
12 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…
Canonical Decision Diagrams Modulo Theories
Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta +1
Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in know…
Effective Prime Factorization via Quantum Annealing by Modular Locally-structured Embedding
Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
This paper investigates novel techniques to solve prime factorization by quantum annealing (QA). Our contribution is twofold. First, we present a novel and very compact modular enc…
Disjoint Partial Enumeration without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one…
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…
Enhancing SMT-based Weighted Model Integration by Structure Awareness
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin +2
The development of efficient exact and approximate algorithms for probabilistic inference is a long-standing goal of artificial intelligence research. Whereas substantial progress…
SMT-based Weighted Model Integration with Structure Awareness
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin +2
Weighted Model Integration (WMI) is a popular formalism aimed at unifying approaches for probabilistic inference in hybrid domains, involving logical and algebraic constraints. Des…