6 citations · 12 across the 8 of their papers we have counts for
8 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…
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…