Document Open Access Logo

A Generalization of the Satisfiability Coding Lemma and Its Applications

Authors Milan Mossé, Harry Sha, Li-Yang Tan

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.9.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Author Details

Milan Mossé
  • Department of Philsophy, University of California Berkeley, CA, USA
Harry Sha
  • Department of Computer Science, University of Toronto, CA
Li-Yang Tan
  • Department of Computer Science, Stanford University, CA, USA

Cite AsGet BibTex

Milan Mossé, Harry Sha, and Li-Yang Tan. A Generalization of the Satisfiability Coding Lemma and Its Applications. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.9

Abstract

The seminal Satisfiability Coding Lemma of Paturi, Pudlák, and Zane is a coding scheme for satisfying assignments of k-CNF formulas. We generalize it to give a coding scheme for implicants and use this generalized scheme to establish new structural and algorithmic properties of prime implicants of k-CNF formulas. Our first application is a near-optimal bound of n⋅ 3^{n(1-Ω(1/k))} on the number of prime implicants of any n-variable k-CNF formula. This resolves an open problem from the Ph.D. thesis of Talebanfard, who proved such a bound for the special case of constant-read k-CNF formulas. Our proof is algorithmic in nature, yielding an algorithm for computing the set of all prime implicants - the Blake Canonical Form - of a given k-CNF formula. The problem of computing the Blake Canonical Form of a given function is a classic one, dating back to Quine, and our work gives the first non-trivial algorithm for k-CNF formulas.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Prime Implicants
  • Satisfiability Coding Lemma
  • Blake Canonical Form
  • k-SAT

Metrics

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

References

  1. Noga Alon and Joel H Spencer. The probabilistic method. John Wiley & Sons, 2004. Google Scholar
  2. Ashok K Chandra and George Markowsky. On the number of prime implicants. Discrete Mathematics, 24(1):7-11, 1978. Google Scholar
  3. Adnan Darwiche and Auguste Hirth. On the reasons behind decisions. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors, ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 712-720. IOS Press, 2020. URL: https://doi.org/10.3233/FAIA200158.
  4. David Déharbe, Pascal Fontaine, Daniel Le Berre, and Bertrand Mazure. Computing prime implicants. In 2013 Formal Methods in Computer-Aided Design, pages 46-52. IEEE, 2013. Google Scholar
  5. B Dunham and R Fridshal. The problem of simplifying logical expressions. The Journal of Symbolic Logic, 24(1):17-19, 1959. Google Scholar
  6. Venkatesan Guruswami, Atri Rudra, and Madhu Sudan. Essential Coding Theory. University at Buffalo, 2012. Google Scholar
  7. Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, and Uri Zwick. Faster k-sat algorithms using biased-PPSZ. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, pages 578-589, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3313276.3316359.
  8. Shuichi Hirahara. A duality between depth-three formulas and approximation by depth-two. arXiv preprint, 2017. URL: http://arxiv.org/abs/1705.03588.
  9. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. Abduction-based explanations for machine learning models. In Pascal Van Hentenryck and Zhi-Hua Zhou, editors, Proceedings of AAAI19-Thirty-Third AAAI conference on Artificial Intelligence, number 1 in Proceedings of the AAAI Conference on Artificial Intelligence, pages 1511-1519, United States of America, 2019. Association for the Advancement of Artificial Intelligence (AAAI). AAAI Conference on Artificial Intelligence 2019, AAAI 2019 ; Conference date: 27-01-2019 Through 01-02-2019. URL: https://doi.org/10.1609/aaai.v33i01.33011511.
  10. Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. On validating, repairing and refining heuristic ML explanations. CoRR, abs/1907.02509, 2019. URL: http://arxiv.org/abs/1907.02509.
  11. Said Jabbour, Joao Marques-Silva, Lakhdar Sais, and Yakoub Salhi. Enumerating prime implicants of propositional formulas in conjunctive normal form. In European Workshop on Logics in Artificial Intelligence, pages 152-165. Springer, 2014. Google Scholar
  12. Vasco M Manquinho, Paulo F Flores, João P Marques Silva, and Arlindo L Oliveira. Prime implicant computation using satisfiability algorithms. In Proceedings Ninth IEEE International Conference on Tools with Artificial Intelligence, pages 232-239. IEEE, 1997. Google Scholar
  13. Joao Marques-Silva, Thomas Gerspacher, Martin C Cooper, Alexey Ignatiev, and Nina Narodytska. Explanations for monotonic classifiers. In International Conference on Machine Learning, pages 7469-7479. PMLR, 2021. Google Scholar
  14. Edward J McCluskey. Minimization of boolean functions. The Bell System Technical Journal, 35(6):1417-1444, 1956. Google Scholar
  15. Peter Bro Miltersen, Jaikumar Radhakrishnan, and Ingo Wegener. On converting CNF to DNF. Theoretical computer science, 347(1-2):325-335, 2005. Google Scholar
  16. Luigi Palopoli, Fiora Pirri, and Clara Pizzuti. Algorithms for selective enumeration of prime implicants. Artificial Intelligence, 111(1-2):41-72, 1999. Google Scholar
  17. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-sat. J. ACM, 52(3):337-364, May 2005. URL: https://doi.org/10.1145/1066100.1066101.
  18. Ramamohan Paturi, Pavel Pudlák, Michael E Saks, and Francis Zane. An improved exponential-time algorithm for k-sat. Journal of the ACM (JACM), 52(3):337-364, 2005. Google Scholar
  19. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. In Proceedings 38th Annual Symposium on Foundations of Computer Science, pages 566-574. IEEE, 1997. Google Scholar
  20. Willard V Quine. The problem of simplifying truth functions. The American mathematical monthly, 59(8):521-531, 1952. Google Scholar
  21. Willard V Quine. Two theorems about truth-functions. Journal of Symbolic Logic, 1954. Google Scholar
  22. Willard V Quine. A way to simplify truth functions. The American mathematical monthly, 62(9):627-631, 1955. Google Scholar
  23. Alexander A Razborov. Bounded arithmetic and lower bounds in boolean complexity. In Feasible Mathematics II, pages 344-386. Springer, 1995. Google Scholar
  24. Daniel Rolf. Derandomization of ppsz for unique-k-sat. In International Conference on Theory and Applications of Satisfiability Testing, pages 216-225. Springer, 2005. Google Scholar
  25. Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI'18, pages 5103-5111. AAAI Press, 2018. Google Scholar
  26. Navid Talebanfard. On the Combinatorics of SAT and the Complexity of Planar Problems. PhD thesis, Department Office Computer Science, Aarhus University, 2014. Google Scholar
  27. Navid Talebanfard. On the structure and the number of prime implicants of 2-CNFs. Discrete Applied Mathematics, 200:1-4, 2016. Google Scholar
  28. Christopher Umans. The minimum equivalent DNF problem and shortest implicants. Journal of Computer and System Sciences, 63(4):597-611, 2001. 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