DROPS

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}
}

Search Results

Documents authored by Sebastiani, Roberto

Entailing Generalization Boosts Enumeration

Abstract

Cite as

On CNF Conversion for Disjoint SAT Enumeration

Abstract

Cite as

Thanks for your feedback!

Could not send message