Document Open Access Logo

Small Unsatisfiable k-CNFs with Bounded Literal Occurrence

Authors Tianwei Zhang , Tomáš Peitl , Stefan Szeider

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.31.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

Tianwei Zhang
  • Algorithms and Complexity Group, TU Wien, Austria
Tomáš Peitl
  • Algorithms and Complexity Group, TU Wien, Austria
Stefan Szeider
  • Algorithms and Complexity Group, TU Wien, Austria

Funding

The project leading to this publication has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 101034440, and was supported by the Austrian Science Fund (FWF) within the project 10.55776/P36688.

Cite AsGet BibTex

Tianwei Zhang, Tomáš Peitl, and Stefan Szeider. Small Unsatisfiable k-CNFs with Bounded Literal Occurrence. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.31

Abstract

We obtain the smallest unsatisfiable formulas in subclasses of k-CNF (exactly k distinct literals per clause) with bounded variable or literal occurrences. Smaller unsatisfiable formulas of this type translate into stronger inapproximability results for MaxSAT in the considered formula class. Our results cover subclasses of 3-CNF and 4-CNF; in all subclasses of 3-CNF we considered we were able to determine the smallest size of an unsatisfiable formula; in the case of 4-CNF with at most 5 occurrences per variable we decreased the size of the smallest known unsatisfiable formula. Our methods combine theoretical arguments and symmetry-breaking exhaustive search based on SAT Modulo Symmetries (SMS), a recent framework for isomorph-free SAT-based graph generation. To this end, and as a standalone result of independent interest, we show how to encode formulas as graphs efficiently for SMS.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Solvers
  • Mathematics of computing → Graph enumeration
  • Theory of computation → Automated reasoning
  • Hardware → Theorem proving and SAT solving
Keywords
  • k-CNF
  • (k,s)-SAT
  • minimally unsatisfiable formulas
  • symmetry breaking

Metrics

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

Related Versions

Supplementary Materials

References

  1. Ron Aharoni and Nathan Linial. Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. J. Combin. Theory Ser. A, 43:196-204, 1986. URL: https://doi.org/10.1016/0097-3165(86)90060-9.
  2. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 167-180. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_18.
  3. Piotr Berman, Marek Karpinski, and Alex D. Scott. Approximation hardness and satisfiability of bounded occurrence instances of SAT. Technical Report TR03-022, Electronic Colloquium on Computational Complexity (ECCC), 2003. URL: https://eccc.weizmann.ac.il/report/2003/022/.
  4. Piotr Berman, Marek Karpinski, and Alexander Scott. Approximation hardness of short symmetric instances of max-3sat. Technical Report TR03-049, Electronic Colloquium on Computational Complexity (ECCC), 2003. URL: https://eccc.weizmann.ac.il/report/2003/049/.
  5. Andreas Darmann and Janosch Döcker. On simplified np-complete variants of monotone3-sat. Discret. Appl. Math., 292:45-58, 2021. URL: https://doi.org/10.1016/J.DAM.2020.12.010.
  6. M. Davis and H. Putnam. A computing procedure for quantification theory. J. of the ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  7. Olivier Dubois. On the r,s-SAT satisfiability problem and a conjecture of Tovey. Discr. Appl. Math., 26(1):51-60, 1990. URL: https://doi.org/10.1016/0166-218X(90)90020-D.
  8. Johannes K. Fichte, Markus Hecher, Daniel Le Berre, and Stefan Szeider. The silent (r)evolution of SAT. Communications of the ACM, 66(6):64-72, June 2023. URL: https://doi.org/10.1145/3560469.
  9. Heidi Gebauer. Disproof of the neighborhood conjecture with implications to SAT. Combinatorica, 32(5):573-587, 2012. URL: https://doi.org/10.1007/S00493-012-2679-Y.
  10. Heidi Gebauer, Tibor Szabó, and Gábor Tardos. The local lemma is asymptotically tight for SAT. J. of the ACM, 63(5):Art. 43, 32, 2016. URL: https://doi.org/10.1145/2975386.
  11. Shlomo Hoory and Stefan Szeider. Computing unsatisfiable k-SAT instances with few occurrences per variable. Theoretical Computer Science, 337(1-3):347-359, 2005. URL: https://doi.org/10.1016/j.tcs.2005.02.004.
  12. Shlomo Hoory and Stefan Szeider. A note on of unsatisfiable k-CNF formulas with few occurrences per variable. SIAM J. Discrete Math., 20(2):523-528, 2006. URL: https://doi.org/10.1137/S0895480104445745.
  13. Matti Järvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  14. Charles Jordan, Will Klieber, and Martina Seidl. Non-cnf QBF solving with QCIR. In Adnan Darwiche, editor, Beyond NP, Papers from the 2016 AAAI Workshop., volume WS-16-05 of AAAI Workshops. AAAI Press, 2016. URL: https://aaai.org/papers/aaaiw-ws0186-16-12601/.
  15. David Jurenka. Upper bounds for (k, s)-SAT. Bachelor’s Thesis, Charles University in Prague, Faculty of Mathematics and Physics, 2011. URL: http://hdl.handle.net/20.500.11956/50583.
  16. Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Co-certificate learning with SAT modulo symmetries. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 1944-1953. ijcai.org, 2023. Main Track. URL: https://doi.org/10.24963/IJCAI.2023/216.
  17. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), LIPIcs, pages 39:1-39:17. Dagstuhl, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.34.
  18. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation and enumeration. ACM Transactions on Computational Logic, 2024. Full and extended version of [Markus Kirchweger and Stefan Szeider, 2021], to appear. Google Scholar
  19. Hans Kleine Büning and Theodor Lettman. Propositional logic: deduction and algorithms. Cambridge University Press, Cambridge, 1999. Google Scholar
  20. Donald E. Knuth. The art of computer programming. Vol. 4B. Combinatorial algorithms. Part 2. Addison-Wesley, Upper Saddle River, NJ, 2023. Google Scholar
  21. Jan Kratochvíl, Petr Savický, and Zsolt Tuza. One more occurrence of variables make satisfiability jump from trivial to NP-complete. SIAM J. Comput., 30:397-403, 1993. URL: https://doi.org/10.1137/0222015.
  22. O. Kullmann. On a generalization of extended resolution. Discrete Appl. Math., 96–97(1):149-176, October 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  23. João P. Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, pages 131-153. IOS Press, 2009. Google Scholar
  24. Hannah Van Santvliet and Ronald de Haan. All instances of monotone 3-sat-(3,1) are satisfiable, 2023. URL: https://arxiv.org/abs/2311.06563.
  25. P. Savický and Jiří Sgall. DNF tautologies with a limited number of occurrences of every variable. Theoretical Computer Science, 238(1-2):495-498, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00036-0.
  26. J. Stříbrná. Between combinatorics and formal logic. Master’s thesis, Charles University, Prague, 1994. Google Scholar
  27. Craig A. Tovey. A simplified NP-complete satisfiability problem. Discr. Appl. Math., 8(1):85-89, 1984. URL: https://doi.org/10.1016/0166-218X(84)90081-7.
  28. Tianwei Zhang, Tomáš Peitl, and Stefan Szeider. Small unsatisfiable k-cnfs with bounded literal occurrence, 2024. URL: https://arxiv.org/abs/2405.16149.
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