Search Results

Documents authored by Spallitta, Giuseppe

Artifact
Software
DOI: 10.4230/artifacts.26304
d-DNNF Modulo Theories - Tool Source Code

Authors: Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani

Abstract
Cite as

Copy BibTex To Clipboard

@misc{dagpub-supp--paper-25314-urlgithub.com-ecivini-tddnnf,
   title = {{d-DNNF Modulo Theories - Tool Source Code}}, 
   author = {Masina, Gabriele and Civini, Emanuele and Michelutti, Massimo and Spallitta, Giuseppe and Sebastiani, Roberto},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:dfb5a8722bba0719e3f4587868462eeb49861e22;origin=https://github.com/ecivini/tddnnf;visit=swh:1:snp:d8c5fef6920b5bfa56c7d89e694ec573e126c93f;anchor=swh:1:rev:f38e4ab6a094249c6ef603f3c212f06c36b17cca}{\texttt{swh:1:dir:dfb5a8722bba0719e3f4587868462eeb49861e22}} (visited on 2026-07-16)},
   url = {https://github.com/ecivini/tddnnf},
}
Artifact
Software
DOI: 10.4230/artifacts.26305
d-DNNF Modulo Theories - Tool Source Code

Authors: Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani

Abstract
Cite as

Copy BibTex To Clipboard

@misc{dagpub-supp--paper-25314-urlgithub.com-ecivini-tddnnf-testbench,
   title = {{d-DNNF Modulo Theories - Tool Source Code}}, 
   author = {Masina, Gabriele and Civini, Emanuele and Michelutti, Massimo and Spallitta, Giuseppe and Sebastiani, Roberto},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:4abff4348814eea939787996676d630614fbcd61;origin=https://github.com/ecivini/tddnnf-testbench;visit=swh:1:snp:f51790b2bcb8ef78b177464f28f7ca7e5234b3bd;anchor=swh:1:rev:5c5f96f133dc43b6575089b3d2f9c85003f6170e}{\texttt{swh:1:dir:4abff4348814eea939787996676d630614fbcd61}} (visited on 2026-07-16)},
   url = {https://github.com/ecivini/tddnnf-testbench},
}
Document
DOI: 10.4230/LIPIcs.SAT.2026.25
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

Authors: Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
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 one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries. In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. As proof of concept, we have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the feasibility and effectiveness of the approach.
Cite as

Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani. d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{masina_et_al:LIPIcs.SAT.2026.25,
  author =	{Masina, Gabriele and Civini, Emanuele and Michelutti, Massimo and Spallitta, Giuseppe and Sebastiani, Roberto},
  title =	{{d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.25},
  URN =		{urn:nbn:de:0030-drops-263316},
  doi =		{10.4230/LIPIcs.SAT.2026.25},
  annote =	{Keywords: SMT, Knowledge Compilation, d-DNNF}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.51
Computing Short SAT Implicants via Ising/QUBO Encodings

Authors: Giuseppe Spallitta, Leonardo Duenas-Osorio, and Moshe Y. Vardi

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Many reasoning tasks require short partial satisfying assignments (implicants), sometimes focusing on a set of important variables. SAT-to-Ising-QUBO formulations are implicitly designed so that ground states correspond to total assignments, since the Ising/QUBO model assigns a value to every spin and has no native representation of unassigned variables. We introduce an Ising/QUBO framework that incorporates "don’t-care" semantics into the quadratic model via a dual-polarity representation, enabling the retrieval of short implicants. The encoding supports implicant shrinking and projection through minor objective modifications. We provide parameter regimes under which ground states correspond to short partial satisfying assignments, achieving minimality and, when the quadratic penalty function permits, minimum-cardinality. We empirically evaluate the encoding with simulated annealing on random 3-SAT enumeration benchmarks and non-CNF formulas, showing that it leaves about one-third of variables unassigned on random 3-SAT formulas while preserving satisfiability, and that consecutive polarity-freezing rounds achieve minimality (and minimum-cardinality) with high probability.
Cite as

Giuseppe Spallitta, Leonardo Duenas-Osorio, and Moshe Y. Vardi. Computing Short SAT Implicants via Ising/QUBO Encodings. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 51:1-51:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{spallitta_et_al:LIPIcs.CP.2026.51,
  author =	{Spallitta, Giuseppe and Duenas-Osorio, Leonardo and Vardi, Moshe Y.},
  title =	{{Computing Short SAT Implicants via Ising/QUBO Encodings}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{51:1--51:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.51},
  URN =		{urn:nbn:de:0030-drops-266843},
  doi =		{10.4230/LIPIcs.CP.2026.51},
  annote =	{Keywords: SAT-to-QUBO, Ising encodings, prime implicants, minimum-cardinality implicant, partial and projected assignments}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.15
On CNF Conversion for Disjoint SAT Enumeration

Authors: Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
Modern SAT 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 of either Tseitin or Plaisted and Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for disjoint SAT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront - which is typically not used in solving - can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.
Cite as

Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. On CNF Conversion for Disjoint SAT Enumeration. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{masina_et_al:LIPIcs.SAT.2023.15,
  author =	{Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
  title =	{{On CNF Conversion for Disjoint SAT Enumeration}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.15},
  URN =		{urn:nbn:de:0030-drops-184775},
  doi =		{10.4230/LIPIcs.SAT.2023.15},
  annote =	{Keywords: CNF conversion, AllSAT, AllSMT}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact