Document Open Access Logo

Resolution with Counting: Dag-Like Lower Bounds and Different Moduli

Authors Fedor Part, Iddo Tzameret

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2020.19.pdf
  • Filesize: 0.78 MB
  • 37 pages

Document Identifiers

Author Details

Fedor Part
  • JetBrains Research, St. Petersburg, Russia
Iddo Tzameret
  • Department of Computer Science, Royal Holloway, University of London, UK

Acknowledgements

We wish to thank Dima Itsykson and Dima Sokolov for very helpful comments concerning this work, and telling us about the lower bound on random $k$-CNF formulas for tree-like Res(lin_{?_2}) that can be achieved using the results of Garlik and Kołodziejczyk. We thank Edward Hirsch for spotting a gap in the initial proof of the dag-like lower bound concerning the use of the contraction.

Cite AsGet BibTex

Fedor Part and Iddo Tzameret. Resolution with Counting: Dag-Like Lower Bounds and Different Moduli. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 19:1-19:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ITCS.2020.19

Abstract

Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), this refutation system operates with disjunctions of linear equations with boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of [Ran Raz and Iddo Tzameret, 2008], through the work of [Dmitry Itsykson and Dmitry Sokolov, 2014] which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. [Jan Krajícek, 2017; Dmitry Itsykson and Dmitry Sokolov, 2014; Jan Krajícek and Igor Carboni Oliveira, 2018; Michal Garlik and Lezsek Kołodziejczyk, 2018]) made it evident that establishing lower bounds against general Res(lin_R) refutations is a challenging and interesting task since the system captures a "minimal" extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds on general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subset-sum principle 1+ x_1 + ̇s +2^n x_n = 0 requires refutations of exponential-size over ℚ. Our proof technique is nontrivial and novel: roughly speaking, we show that under certain conditions every refutation of a subset-sum instance f=0, where f is a linear polynomial over ℚ, must pass through a fat clause containing an equation f=α for each α in the image of f under boolean assignments. We develop a somewhat different approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. We then turn to the finite fields regime, showing that the work of Itsykson and Sokolov [Dmitry Itsykson and Dmitry Sokolov, 2014] who obtained tree-like lower bounds over ?_2 can be carried over and extended to every finite field. We establish new lower bounds and separations as follows: (i) for every pair of distinct primes p,q, there exist CNF formulas with short tree-like refutations in Res(lin_{?_p}) that require exponential-size tree-like Res(lin_{?_q}) refutations; (ii) random k-CNF formulas require exponential-size tree-like Res(lin_{?_p}) refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like Res(lin_?) refutations of the pigeonhole principle, for every field ?.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • concrete lower bounds
  • resolution
  • satisfiability
  • combinatorics

Metrics

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

Related Versions

References

  1. Miklós Ajtai. The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science, pages 346-355, 1988. Google Scholar
  2. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: non-binomial case. In Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science (Las Vegas, NV, 2001), pages 190-199. IEEE Computer Soc., Los Alamitos, CA, 2001. Google Scholar
  3. Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret. Semi-Algebraic Proofs, IPS Lower Bounds and the τ-Conjecture: Can a Natural Number be Negative? Electronic Colloquium on Computational Complexity TR19-142, 2019. Google Scholar
  4. Noga Alon and Zoltán Füredi. Covering the Cube by Affine Hyperplanes. Eur. J. Comb., 14(2):79-83, March 1993. URL: https://doi.org/10.1006/eujc.1993.1011.
  5. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing Planes. In Anna R. Karlin, editor, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018), volume 94 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:20, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITCS.2018.10.
  6. Paul Beame, Henry A. Kautz, and Ashish 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.
  7. Eli Ben-Sasson. Hard examples for the bounded depth Frege proof system. Comput. Complexity, 11(3-4):109-136, 2002. Google Scholar
  8. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  9. Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. System Sci., 62(2):267-289, 2001. Special issue on the 14th Annual IEEE Conference on Computational Complexity (Atlanta, GA, 1999). Google Scholar
  10. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996), pages 174-183, New York, 1996. ACM. Google Scholar
  11. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. J. Symb. Log., 44(1):36-50, 1979. This is a journal-version of Reckhow [Robert Reckhow, 1976]. URL: https://doi.org/10.2307/2273702.
  12. Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof Complexity Lower Bounds from Algebraic Circuit Complexity. In 31st Conference on Computational Complexity, CCC 2016, May 29 to June 1, 2016, Tokyo, Japan, pages 32:1-32:17, 2016. URL: https://doi.org/10.4230/LIPIcs.CCC.2016.32.
  13. Michal Garlik and Lezsek Kołodziejczyk. Some Subsystems of Constant-Depth Frege with Parity. ACM Transactions on Computational Logic, 19(4), 2018. URL: https://www.mimuw.edu.pl/~lak/jansparity.pdf.
  14. 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.
  15. Armin Haken. The intractability of resolution. Theoret. Comput. Sci., 39(2-3):297-308, 1985. Google Scholar
  16. J. Hastad. On Small-Depth Frege Proofs for Tseitin for Grids. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pages 97-108, Los Alamitos, CA, USA, October 2017. IEEE Computer Society. URL: https://doi.org/10.1109/FOCS.2017.18.
  17. Dmitry Itsykson and Dmitry Sokolov. Lower Bounds for Splittings by Linear Combinations. In Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, pages 372-383, 2014. URL: https://doi.org/10.1007/978-3-662-44465-8_32.
  18. Jan Krajícek. A feasible interpolation for random resolution. Logical Methods in Computer Science, 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:5)2017.
  19. Jan Krajícek and Igor Carboni Oliveira. On monotone circuits with local oracles and clique lower bounds. Chicago J. Theor. Comput. Sci., 2018, 2018. URL: http://cjtcs.cs.uchicago.edu/articles/2018/1/contents.html.
  20. Jan Krajíček, Pavel Pudlák, and Alan Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures Algorithms, 7(1):15-39, 1995. Google Scholar
  21. Nathan Linial and Jaikumar Radhakrishnan. Essential covers of the cube by hyperplanes. Journal of Combinatorial Theory, Series A, 109:331-338, 2005. Google Scholar
  22. A. Lubotzky, R. Phillips, and P. Sarnak. Ramanujan graphs. Combinatorica, 8(3):261-277, September 1988. URL: https://doi.org/10.1007/BF02126799.
  23. Jakob Nordström. On the Interplay Between Proof Complexity and SAT Solving. ACM SIGLOG News, 2(3):19-44, August 2015. URL: https://doi.org/10.1145/2815493.2815497.
  24. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. Comput. Complexity, 3(2):97-140, 1993. Google Scholar
  25. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-SAT (preliminary version). In Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9-11, 2000, San Francisco, CA, USA., pages 128-136, 2000. URL: http://dl.acm.org/citation.cfm?id=338219.338244.
  26. 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.
  27. Robert Reckhow. On the lengths of proofs in the propositional calculus. PhD thesis, University of Toronto, 1976. Technical Report No . 87. Google Scholar
  28. Grigori Tseitin. On the complexity of derivations in propositional calculus, pages 466-483. Studies in constructive mathematics and mathematical logic Part II. Consultants Bureau, New-York-London, 1968. 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