[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

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

  • Published:
computational complexity Aims and scope Submit manuscript

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 \({\rm Res}({\rm 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 Raz & Tzameret (2008), through the work of Itsykson & Sokolov (2020) which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. Garlik & Kołodziejczyk 2018; Itsykson & Sokolov 2020; Krajícek 2017; Krajícek & Oliveira 2018) made it evident that establishing lower bounds against general \({\rm Res}({\rm 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 against general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular, we prove that the subset-sum principle \(1+\sum\nolimits_{i=1}^{n}2^i x_i = 0\) requires refutations of exponential size over \(\mathbb{Q}\). We use a novel lower bound technique: We show that under certain conditions every refutation of a subset-sum instance \(f=0\) must pass through a fat clause consisting of the equation \(f=\alpha\) for every \(\alpha\) in the image of f under Boolean assignments, or can be efficiently reduced to a proof containing such a clause. We then modify this 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 & Sokolov (2020), where tree-like lower bounds over \(\mathbb{F}_2\) were obtained, 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 \({\rm Res}({\rm lin}{\mathbb{F}_p})\) that require exponential-size tree-like \({\rm Res}({\rm lin}{\mathbb{F}_q})\) refutations; (ii) random k-CNF formulas require exponential-size tree-like \({\rm Res}({\rm lin}{\mathbb{F}_p})\) refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like \({\rm Res}({\rm lin}{\mathbb{F}})\) refutations of the pigeonhole principle, for every field \(\mathbb{F}\).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Miklós Ajtai (1988). The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science, 346–355

  • Michael Alekhnovich & Alexander A. Razborov (2001). Lower bounds for polynomial calculus: non-binomial case. In Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science (Las Vegas, NV, 2001), 190–199. IEEE Computer Soc., Los Alamitos, CA

  • Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch & Iddo Tzameret (2020). Semi-Algebraic Proofs, IPS Lower Bounds and the \(\tau\)-Conjecture: Can a Natural Number be Negative? STOC 2020

  • Noga Alon & Zoltán Füredi (1993). Covering the Cube by Affine Hyperplanes. Eur. J. Comb. 14(2), 79–83. ISSN 0195-6698. URL http://dx.doi.org/10.1006/eujc.1993.1011

  • Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi & Robert Robere (2018). Stabbing Planes. In 9th Innovations in Theoretical Computer Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, Anna R. Karlin, editor, volume 94 of LIPIcs, 10:1–10:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL https://doi.org/10.4230/LIPIcs.ITCS.2018.10

  • Paul Beame, Henry A. Kautz & Ashish Sabharwal (2004). Towards Understanding and Harnessing the Potential of Clause Learning. J. Artif. Intell. Res. 22, 319–351. URL https://doi.org/10.1613/jair.1410

  • Eli Ben-Sasson (2002). Hard examples for the bounded depth Frege proof system. Comput. Complexity 11(3-4), 109–136. ISSN 1016-3328

  • Eli Ben-Sasson & Avi Wigderson (2001). Short proofs are narrow– resolution made simple. J. ACM 48(2), 149–169

    Article  MathSciNet  Google Scholar 

  • Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo & Toniann Pitassi (2001). Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. System Sci. 62(2), 267–289. ISSN 0022-0000. Special issue on the 14th Annual IEEE Conference on Computational Complexity (Atlanta, GA, 1999)

  • Matthew Clegg, Jeffery Edmonds & Russell Impagliazzo (1996). 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), 174–183. ACM, New York

  • Stephen A. Cook & Robert A. Reckhow (1974a). Corrections for "On the Lengths of Proofs in the Propositional Calculus (Preliminary Version)". SIGACT News 6(3), 15–22

    Article  Google Scholar 

  • Stephen A. Cook & Robert A. Reckhow (1974b). On the Lengths of Proofs in the Propositional Calculus (Preliminary Version). In STOC1974, 135–148. For corrections see Cook–Reckhow Cook & Reckhow (1974a)

  • Stephen A. Cook & Robert A. Reckhow (1979). The Relative Efficiency of Propositional Proof Systems. J. Symb. Log. 44(1), 36–50

    Article  MathSciNet  Google Scholar 

  • This is a journal-version of Cook–Reckhow Cook & Reckhow (1974b) and Reckhow Reckhow (1976)

  • Michael A. Forbes, Amir Shpilka, Iddo Tzameret & Avi Wigderson (2016). Proof Complexity Lower Bounds from Algebraic Circuit Complexity. In 31st Conference on Computational Complexity, CCC 2016, May 29 to June 1, 2016, Tokyo, Japan, 32:1–32:17. URL http://dx.doi.org/10.4230/LIPIcs.CCC.2016.32

  • Michal Garlik & Lezsek Kołodziejczyk (2018). Some Subsystems of Constant-Depth Frege with Parity. ACM Transactions on Computational Logic 19(4). URL https://www.mimuw.edu.pl/~lak/jansparity.pdf

  • Joshua A. Grochow & Toniann Pitassi (2018). Circuit Complexity, Proof Complexity, and Polynomial Identity Testing: The Ideal Proof System. J. ACM 65(6), 37:1–37:59. URL https://doi.org/10.1145/3230742

  • Armin Haken (1985). The intractability of resolution. Theoret. Comput. Sci. 39(2-3), 297–308. ISSN 0304-3975

  • Johan Håstad (2017). On Small-Depth Frege Proofs for Tseitin for Grids. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, 97–108. URL https://doi.org/10.1109/FOCS.2017.18

  • Dmitry Itsykson & Dmitry Sokolov (2020). Resolution over linear equations modulo two. In Ann. Pure Appl. Log. 171(1). URL https://doi.org/10.1016/j.apal.2019.102722

  • Jan Krajíček (1998). Discretely ordered modules as a first-order extension of the cutting planes proof system. The Journal of Symbolic Logic 63(4), 1582–1596. ISSN 0022-4812

  • Jan Krajícek (2017). A feasible interpolation for random resolution. Logical Methods in Computer Science 13(1). URL https://doi.org/10.23638/LMCS-13(1:5)2017

  • Jan Krajícek & Igor Carboni Oliveira (2018). On monotone circuits with local oracles and clique lower bounds. Chicago J. Theor. Comput. Sci. 2018. URL http://cjtcs.cs.uchicago.edu/articles/2018/1/contents.html

  • Jan Krajíček, Pavel Pudlák & Alan Woods (1995). An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures Algorithms 7(1), 15–39. ISSN 1042-9832

  • Nathan Linial & Jaikumar Radhakrishnan (2005). Essential covers of the cube by hyperplanes. Journal of Combinatorial Theory, Series A 109, 331–338

    Article  MathSciNet  Google Scholar 

  • A. Lubotzky, R. Phillips & P. Sarnak (1988). Ramanujan graphs. Combinatorica 8(3), 261–277. ISSN 1439-6912. URL https://doi.org/10.1007/BF02126799

  • Jakob Nordström (2015). On the Interplay Between Proof Complexity and SAT Solving. ACM SIGLOG News 2(3), 19–44. ISSN 2372-3491. URL http://doi.acm.org/10.1145/2815493.2815497

  • Fedor Part & Iddo Tzameret (2020). Resolution with Counting: Dag-Like Lower Bounds and Different Moduli. In 11th Innovations in Theoretical Computer Science Conference, ITCS 2020, January 12-14, 2020, Seattle, Washington, USA, Thomas Vidick, editor, volume 151 of LIPIcs, 19:1–19:37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL https://doi.org/10.4230/LIPIcs.ITCS.2020.19

  • Toniann Pitassi, Paul Beame & Russell Impagliazzo (1993). Exponential lower bounds for the pigeonhole principle. Comput. Complexity 3(2), 97–140. ISSN 1016-3328

  • Pavel Pudlák & Russell Impagliazzo (2000). 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., 128–136. URL http://dl.acm.org/citation.cfm?id=338219.338244

  • Ran Raz & Iddo Tzameret (2008). Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic 155(3), 194–224. URL http://dx.doi.org/10.1016/j.apal.2008.04.001

  • Robert A. Reckhow (1976). On the lengths of proofs in the propositional calculus. Ph.D. thesis, University of Toronto. URL https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf

  • Grigori Tseitin (1968). On the complexity of derivations in propositional calculus. Studies in constructive mathematics and mathematical logic Part II. Consultants Bureau, New-York-London

    MATH  Google Scholar 

Download references

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\(({\rm lin}_{\mathbb{F}_{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 rule, and Fedor Petrov for very useful discussions. Lastly, we are grateful to the anonymous reviewers of the extended abstract as well as the journal version of this work, who contributed to improving the exposition. An extended abstract of this paper has appeared as Part & Tzameret (2020).

Author information

Authors and Affiliations

  1. JetBrains Research, St. Petersburg, Russia

    Fedor Part

  2. Department of Computer Science Royal Holloway, University of London, London, UK

    Iddo Tzameret

Authors
  1. Fedor Part
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Iddo Tzameret
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fedor Part .

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Part , F., Tzameret, I. Resolution with Counting: Dag-Like Lower Bounds and Different Moduli. comput. complex. 30, 2 (2021). https://doi.org/10.1007/s00037-020-00202-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s00037-020-00202-x

Keywords

Subject classification

Search

Navigation