Search Results

Documents authored by Sebastiani, Roberto

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.SAT.2024.13
Entailing Generalization Boosts Enumeration

Authors: Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.
Cite as

Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing Generalization Boosts Enumeration. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fried_et_al:LIPIcs.SAT.2024.13,
  author =	{Fried, Dror and Nadel, Alexander and Sebastiani, Roberto and Shalmon, Yogev},
  title =	{{Entailing Generalization Boosts Enumeration}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{13:1--13:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.13},
  URN =		{urn:nbn:de:0030-drops-205351},
  doi =		{10.4230/LIPIcs.SAT.2024.13},
  annote =	{Keywords: Generalization, Minimization, Prime Implicant, AllSAT, SAT, Circuits}
}
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