Document Open Access Logo

Proving Unsatisfiability with Hitting Formulas

Authors Yuval Filmus , Edward A. Hirsch , Artur Riazanov , Alexander Smal , Marc Vinyals

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2024.48.pdf
  • Filesize: 0.83 MB
  • 20 pages

Document Identifiers

Author Details

Yuval Filmus
  • Technion - Israel Institute of Technology, Haifa, Israel
Edward A. Hirsch
  • Department of Computer Science, Ariel University, Israel
Artur Riazanov
  • EPFL, Lausanne, Switzerland
Alexander Smal
  • Technion - Israel Institute of Technology, Haifa, Israel
Marc Vinyals
  • University of Auckland, New Zealand

Funding

This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 802020-ERC-HARMONIC.
  • Riazanov, Artur: This work was supported by the Swiss State Secretariat for Education, Research and Innovation (SERI) under contract number MB22.00026.

Acknowledgements

We thank Jan Johannsen, Ilario Bonacina, Oliver Kullmann, and Stefan Szeider for introducing us to the topic; Zachary Chase, Susanna de Rezende, Mika Göös, Amir Shpilka, and Dmitry Sokolov for helpful discussions.

Cite AsGet BibTex

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITCS.2024.48

Abstract

A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • hitting formulas
  • polynomial identity testing
  • query complexity

Metrics

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

Related Versions

References

  1. Scott Aaronson, Shalev Ben-David, and Robin Kothari. Separations in query complexity using cheat sheets. In STOC-2016, pages 863-876, 2016. URL: https://doi.org/10.1145/2897518.2897644.
  2. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM Journal on Computing, 31(4):1184-1211, 2002. URL: https://doi.org/10.1137/S0097539700366735.
  3. Yaroslav Alekseev. A lower bound for polynomial calculus with extension rule. In 36th Computational Complexity Conference, volume 200 of LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., 2021. Art. 21:18. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.21.
  4. Andris Ambainis, Martins Kokainis, and Robin Kothari. Nearly optimal separations between communication (or query) complexity and partitions. In 31st Conference on Computational Complexity, volume 50 of LIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 4, 14. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2016. URL: https://doi.org/10.4230/LIPIcs.CCC.2016.4.
  5. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. System Sci., 74(3):323-334, 2008. URL: https://doi.org/10.1016/j.jcss.2007.06.025.
  6. Boaz Barak and David Steurer. Sum-of-squares proofs and the quest toward optimal algorithms. ECCC, TR14-059, 2014. URL: https://eccc.weizmann.ac.il/report/2014/059, URL: https://arxiv.org/abs/TR14-059.
  7. P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi, and P. Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc., 73(3):1-26, 1996. URL: https://doi.org/10.1112/plms/s3-73.1.1.
  8. P. Beame, H. A. Kautz, and A. Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res., 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  9. P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In 37th Conference on Foundations of Computer Science, pages 274-282, 1996. URL: https://doi.org/10.1109/SFCS.1996.548486.
  10. Paul Beame and Sajin Koroth. On disperser/lifting properties of the index and inner-product functions, 2022. URL: https://arxiv.org/abs/2211.17211.
  11. Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower bounds for Lovász-Schrijver systems and beyond follow from multiparty communication complexity. In Automata, Languages and Programming, volume 3580 of LNCS, pages 1176-1188. Springer, 2005. Google Scholar
  12. Paul Beame and Søren Riis. More on the relative strength of counting principles. In Proof Complexity and Feasible Arithmetics, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 13-35, 1996. URL: https://doi.org/10.1090/dimacs/039/02.
  13. Eli Ben-Sasson. Size-space tradeoffs for resolution. SIAM Journal on Computing, 38(6):2511-2525, 2009. URL: https://doi.org/10.1137/080723880.
  14. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585-603, 2004. URL: https://doi.org/10.1007/s00493-004-0036-5.
  15. Archie Blake. Canonical expressions in Boolean algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  16. Josh Buresh-Oppenheim, Matthew Clegg, Russell Impagliazzo, and Toniann Pitassi. Homogenization and the polynomial calculus. Comput. Complex., 11(3-4):91-108, 2002. URL: https://doi.org/10.1007/s00037-002-0171-6.
  17. Arkadev Chattopadhyay, Nikhil S. Mande, Swagato Sanyal, and Suhail Sherif. Lifting to parity decision trees via stifling, 2022. URL: https://arxiv.org/abs/2211.17214.
  18. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In 28th Annual ACM Symposium on the Theory of Computing, pages 174-183, New York, 1996. ACM. URL: https://doi.org/10.1145/237814.237860.
  19. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  20. W. Cook, C. R. Coullard, and G. Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. Google Scholar
  21. E. Dantsin and E. A. Hirsch. Worst-case upper bounds. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, 2nd Ed., volume 336 of Frontiers in Artificial Intelligence and Applications, pages 669-692. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200999.
  22. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962. Google Scholar
  23. M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. Google Scholar
  24. G. Davydov and I. Davydova. Dividing formulas and polynomial classes for satisfiability. In SAT’98, 2nd Workshop on the Satisfiability Problem, pages 12-21, 1998. Google Scholar
  25. S.F. de Rezende, J. Nordström, and M. Vinyals. How limited interaction hinders real communication (and what it means for proof and circuit complexity). In 57th Annual Symposium on Foundations of Computer Science, pages 295-304, 2016. URL: https://doi.org/10.1109/FOCS.2016.40.
  26. Susanna F. de Rezende. Automating tree-like resolution in time n^o(log n) is ETH-hard. Procedia Computer Science, 195:152-162, 2021. Proceedings of the XI Latin and American Algorithms, Graphs and Optimization Symposium. URL: https://doi.org/10.1016/j.procs.2021.11.021.
  27. Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The power of negative reasoning. In 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 40:1-40:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.40.
  28. Andrzej Ehrenfeucht and David Haussler. Learning decision trees from random examples. Inform. and Comput., 82(3):231-246, 1989. URL: https://doi.org/10.1016/0890-5401(89)90001-1.
  29. Y. Filmus, E. A. Hirsch, S. Kurz, F. Ihringer, A. Ryazanov, A. V. Smal, and M. Vinyals. Irreducible subcube partitions. Electron. J. Comb., 30(3), 2023. URL: https://doi.org/10.37236/11862.
  30. N. Fleming, P. Kothari, and T. Pitassi. Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comput. Sci., 14(1-2):1-221, 2019. URL: https://doi.org/10.1561/0400000086.
  31. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. Theory Comput., 16(13):1-30, 2020. URL: https://doi.org/10.4086/toc.2020.v016a013.
  32. Michal Garlík and Leszek Aleksander Kołodziejczyk. Some subsystems of constant-depth Frege with parity. ACM Trans. Comput. Logic, 19(4), November 2018. URL: https://doi.org/10.1145/3243126.
  33. Mika Göös, Stefan Kiefer, and Weiqiang Yuan. Lower Bounds for Unambiguous Automata via Communication Complexity. In 49th International Colloquium on Automata, Languages, and Programming, volume 229 of LIPIcs. Leibniz Int. Proc. Inform., pages 126:1-126:13. Schloss Dagstuhl. Leibniz-Zent. Inform., 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.126.
  34. Dima Grigoriev and Edward A. Hirsch. Algebraic proof systems over formulas. Theoret. Comput. Sci., 303(1):83-102, 2003. Logic and complexity in computer science (Créteil, 2001). URL: https://doi.org/10.1016/S0304-3975(02)00446-2.
  35. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1-37:59, 2018. URL: https://doi.org/10.1145/3230742.
  36. Svyatoslav Gryaznov. Notes on resolution over linear equations. In CSR-2019, volume 11532 of LNCS, pages 168-179. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-19955-5_15.
  37. Matthew Gwynne. Hierarchies for efficient clausal entailment checking: With applications to satisfiability and knowledge compilation. PhD thesis, Swansea University, 2014. Google Scholar
  38. Matthew Gwynne and Oliver Kullmann. Towards a theory of good SAT representations. CoRR, abs/1302.4421, 2013. URL: http://arxiv.org/abs/1302.4421, URL: https://arxiv.org/abs/1302.4421.
  39. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP, 2022. URL: https://arxiv.org/abs/2205.02168.
  40. Mika Göös, Toniann Pitassi, and Thomas Watson. Query-to-communication lifting for bpp. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pages 132-143, 2017. URL: https://doi.org/10.1109/FOCS.2017.21.
  41. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. Google Scholar
  42. Trinh Huynh and Jakob Nordström. On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity. In 44th Annual ACM Symposium on Theory of Computing, pages 233-248, 2012. URL: https://doi.org/10.1145/2213977.2214000.
  43. Dmitry Itsykson and Artur Riazanov. Proof Complexity of Natural Formulas via Communication Arguments. In 36th Computational Complexity Conference (CCC 2021), volume 200 of LIPIcs. Leibniz Int. Proc. Inform., pages 3:1-3:34, Dagstuhl, Germany, 2021. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.3.
  44. Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Ann. Pure Appl. Logic, 171(1):102722, 31, 2020. URL: https://doi.org/10.1016/j.apal.2019.102722.
  45. Kazuo Iwama. CNF-satisfiability test by counting and polynomial average time. SIAM J. Comput., 18(2):385-391, 1989. URL: https://doi.org/10.1137/0218026.
  46. Rahul Jain and Hartmut Klauck. The partition bound for classical communication complexity and query complexity. In 25th Annual IEEE Conference on Computational Complexity, pages 247-258, 2010. URL: https://doi.org/10.1109/CCC.2010.31.
  47. Jan Krajíček. Discretely ordered modules as a first-order extension of the cutting planes proof system. Journal of Symbolic Logic, 63(4):1582-1596, 1998. URL: https://doi.org/10.2307/2586668.
  48. Oliver Kullmann. The combinatorics of conflicts between clauses. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing (SAT 2003), volume 2919 of LNCS, pages 426-440. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24605-3_32.
  49. Oliver Kullmann. Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure. Fundam. Informaticae, 109(1):83-119, 2011. URL: https://doi.org/10.3233/FI-2011-429.
  50. Oliver Kullmann and Xishun Zhao. On Davis-Putnam reductions for minimally unsatisfiable clause-sets. Theoret. Comput. Sci., 492:70-87, 2013. URL: https://doi.org/10.1016/j.tcs.2013.04.020.
  51. Eyal Kushilevitz and Noam Nisan. Communication complexity. CUP, 1997. Google Scholar
  52. Noam Nisan and Mario Szegedy. On the degree of boolean functions as real polynomials. Computational Complexity, 4, 1995. URL: https://doi.org/10.1145/129712.129757.
  53. Tomás Peitl and Stefan Szeider. Are hitting formulas hard for resolution? CoRR, abs/2206.15225, 2022. URL: https://doi.org/10.48550/arXiv.2206.15225.
  54. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  55. Toniann Pitassi. Algebraic propositional proof systems. In Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 215-244. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/031/07.
  56. Pavel Pudlák. Proofs as games. Am. Math. Mon., 107(6):541-550, 2000. URL: http://www.jstor.org/stable/2589349.
  57. Ran Raz and Amir Shpilka. Deterministic polynomial identity testing in non-commutative models. Comput. Complexity, 14(1):1-19, 2005. URL: https://doi.org/10.1007/s00037-005-0188-8.
  58. Ran Raz and Iddo Tzameret. Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic, 155(3):194-224, 2008. URL: https://doi.org/10.1016/j.apal.2008.04.001.
  59. R. A. Reckhow. On the Lengths of Proofs in the Propositional Calculus. PhD thesis, University of Toronto, 1976. URL: https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf.
  60. Suhail Sherif. Communication Complexity and Quantum Optimization Lower Bounds via Query Complexity. PhD thesis, Tata Institute of Fundamental Research, Mumbai, 2021. Google Scholar
  61. Dmitry Sokolov. Dag-like communication and its applications. In CSR-2017, volume 10304 of LNCS, pages 294-307. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-58747-9_26.
  62. G. S. Tseitin. On the complexity of derivation in the propositional calculus. Zapiski nauchnykh seminarov LOMI, 8:234-259, 1968. Translation: Consultants Bureau, N.Y., 1970, pp. 115-125. Google Scholar
  63. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
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