Document Open Access Logo

On CNF Conversion for Disjoint SAT Enumeration

Authors Gabriele Masina , Giuseppe Spallitta , Roberto Sebastiani

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.15.pdf
  • Filesize: 1.97 MB
  • 16 pages

Document Identifiers

Author Details

Gabriele Masina
  • DISI, University of Trento, Italy
Giuseppe Spallitta
  • DISI, University of Trento, Italy
Roberto Sebastiani
  • DISI, University of Trento, Italy

Funding

We acknowledge the support of the MUR PNRR project FAIR - Future AI Research (PE00000013), under the NRRP MUR program funded by the NextGenerationEU. The work was partially supported by the project "AI@TN" funded by the Autonomous Province of Trento.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.SAT.2023.15

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Hardware → Theorem proving and SAT solving
  • Computing methodologies → Representation of Boolean functions
Keywords
  • CNF conversion
  • AllSAT
  • AllSMT

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. A. Biere and H. van Maaren. Handbook of Satisfiability: Second Edition. IOS Press, May 2021. Google Scholar
  2. Magnus Björk. Successful SAT Encoding Techniques. Journal on Satisfiability, Boolean Modeling and Computation, 7(4):189-201, July 2009. Google Scholar
  3. Thierry Boy de la Tour. An Optimality Result for Clause Form Translation. Journal of Symbolic Computation, 14(4):283-301, October 1992. Google Scholar
  4. F. Brglez and H. Fujiwara. A Neutral Netlist of 10 Combinational Benchmark Circuits and a Target Translator in Fortran. In Proceedings of IEEE International Symposium Circuits and Systems (ISCAS 85), pages 677-692. IEEE Press, Piscataway, N.J., 1985. Google Scholar
  5. Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate Counting in SMT and Value Estimation for Probabilistic Programs. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035, pages 320-334, New York, NY, USA, 2015. Springer-Verlag New York, Inc. Google Scholar
  6. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 93-107. Springer, 2013. Google Scholar
  7. Marco Gario and Andrea Micheli. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop 2015, 2015. Google Scholar
  8. M.C. Hansen, H. Yalcin, and J.P. Hayes. Unveiling the ISCAS-85 benchmarks: a case study in reverse engineering. IEEE Design & Test of Computers, 16(3):72-80, 1999. Google Scholar
  9. Markus Iser, Carsten Sinz, and Mana Taghdiri. Minimizing Models for Tseitin-Encoded SAT Instances. In Theory and Applications of Satisfiability Testing – SAT 2013, volume 7962, pages 224-232. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. Series Title: LNCS. Google Scholar
  10. Paul Jackson and Daniel Sheridan. The Optimality of a Fast CNF Conversion and its Use with SAT. In Theory and Applications of Satisfiability Testing – SAT 2004, 2004. Google Scholar
  11. Elias Kuiter, Sebastian Krieter, Chico Sundermann, Thomas Thüm, and Gunter Saake. Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses. In 37th IEEE/ACM Int. Conference on Automated Software Engineering, pages 1-13. ACM, 2022. Google Scholar
  12. Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras. SMT Techniques for Fast Predicate Abstraction. In Computer Aided Verification, volume 4144 of Lecture Notes in Computer Science, pages 424-437. Springer Berlin Heidelberg, 2006. Google Scholar
  13. Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. On CNF Conversion for SAT Enumeration, June 2023. URL: https://arxiv.org/abs/2303.14971.
  14. Paolo Morettin, Andrea Passerini, and Roberto Sebastiani. Efficient Weighted Model Integration via SMT-Based Predicate Abstraction. In Proceedings of the 26th International Joint Conference on Artificial Intelligence, pages 720-728, 2017. Google Scholar
  15. Paolo Morettin, Andrea Passerini, and Roberto Sebastiani. Advanced SMT techniques for Weighted Model Integration. Artificial Intelligence, 275(C):1-27, 2019. Google Scholar
  16. Sibylle Möhle, Roberto Sebastiani, and Armin Biere. Four Flavors of Entailment. In Theory and Applications of Satisfiability Testing - SAT 2020, Lecture Notes in Computer Science, pages 62-71. Springer, 2020. Google Scholar
  17. David A. Plaisted and Steven Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2(3):293-304, 1986. Google Scholar
  18. Roberto Sebastiani. Are You Satisfied by This Partial Assignment?, 2020. URL: https://arxiv.org/abs/2003.04225.
  19. Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, and Roberto Sebastiani. SMT-based Weighted Model Integration with Structure Awareness. In Proceedings of the 38th Conference on Uncertainty in Artificial Intelligence, volume 180, pages 1876-1885, 2022. Google Scholar
  20. Abraham Temesgen Tibebu and Goerschwin Fey. Augmenting All Solution SAT Solving for Circuits with Structural Information. In IEEE 21st International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS), pages 117-122, 2018. Google Scholar
  21. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of Reasoning 2: Classical Papers on Computational Logic 1967-70, pages 466-483. Springer, 1983. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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