More Web Proxy on the site http://driver.im/

research-article

Some Subsystems of Constant-Depth Frege with Parity

Authors:

Michal Garlík,

Leszek Aleksander KołodziejczykAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 19, Issue 4

Article No.: 29, Pages 1 - 34

https://doi.org/10.1145/3243126

Published: 20 November 2018 Publication History

Abstract

We consider three relatively strong families of subsystems of AC⁰[2]-Frege proof systems, i.e., propositional proof systems using constant-depth formulas with an additional parity connective, for which exponential lower bounds on proof size are known. In order of increasing strength, the subsystems are (i) constant-depth proof systems with parity axioms and the (ii) treelike and (iii) daglike versions of systems introduced by Krajíček which we call PK^c_d(⊕). In a PK^c_d(⊕)-proof, lines are disjunctions (cedents) in which all disjuncts have depth at most d, parities can only appear as the outermost connectives of disjuncts, and all but c disjuncts contain no parity connective at all.

We prove that treelike PK^O(1)_O(1)(⊕) is quasipolynomially but not polynomially equivalent to constant-depth systems with parity axioms. We also verify that the technique for separating parity axioms from parity connectives due to Impagliazzo and Segerlind can be adapted to give a superpolynomial separation between daglike PK^O(1)_O(1)(⊕) and AC⁰[2]-Frege; the technique is inherently unable to prove superquasipolynomial separations.

We also study proof systems related to the system Res-Lin introduced by Itsykson and Sokolov. We prove that an extension of treelike Res-Lin is polynomially simulated by a system related to daglike PK^O(1)_O(1)(⊕), and obtain an exponential lower bound for this system.

References

[1]

Albert Atserias, Moritz Müller, and Sergi Oliva. 2015. Lower bounds for DNF-refutations of a relativized weak pigeonhole principle. Journal of Symbolic Logic 80, 2 (2015), 450--476.

[2]

Paul Beame. 1994. A Switching Lemma Primer. Technical Report UW-CSE-95-07-01. University of Washington, Department of Computer Science and Engineering.

[3]

Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. 1996. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proceedings of the London Mathematical Society 73, 3 (1996), 1--26.

[4]

Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák, and Alan R. Woods. 1992. Exponential lower bounds for the pigeonhole principle. In Proceedings of the 24th ACM Symposium on Theory of Computing. ACM, 200--220.

Digital Library

[5]

Paul Beame and Søren Riis. 1997. More on the relative strength of counting principles. In Proof Complexity and Feasible Arithmetics, P. Beame and S. Buss (Eds.). American Mathematical Society, 13--36.

[6]

Arnold Beckmann and Jan Johannsen. 2005. An unexpected separation result in linearly bounded arithmetic. Mathematical Logic Quarterly 51, 2 (2005), 191--200.

[7]

Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow -- Resolution made simple. Journal of the ACM 48, 2 (2001), 149--169.

Digital Library

[8]

Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. 2001. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences 62, 2 (2001), 267--289.

Digital Library

[9]

Samuel R. Buss. 1998. Lower bounds on nullstellensatz proofs via designs. In Proof Complexity and Feasible Arithmetics (Rutgers, NJ, 1996). DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, Vol. 39. American Mathematical Society, Providence, RI, 59--71.

[10]

S. R. Buss. 2012. Towards NP-P via proof complexity and search. Annals of Pure and Applied Logic 163, 7 (2012), 906--917.

[11]

Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall. 1996/1997. Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Computational Complexity 6 (1996/1997), 256--298.

Digital Library

[12]

Samuel R. Buss, Leszek Aleksander Kołodziejczyk, and Konrad Zdanowski. 2015. Collapsing modular counting in bounded arithmetic and constant depth propositional proofs. Transactions of the American Mathematical Society 367, 11 (2015), 7517--7563.

[13]

Samuel R. Buss and Toniann Pitassi. 1998. Good degree bounds on nullstellensatz refutations of the induction principle. Journal of Computer and System Sciences 57, 2 (1998), 162--171.

Digital Library

[14]

Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. 1996. Using the groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of STOC 1996. ACM, 174--183.

Digital Library

[15]

Nicola Galesi and Massimo Lauria. 2010. Optimality of size-degree tradeoffs for polynomial calculus. ACM Transactions on Computational Logic 12, 1 (2010), Article 4.

Digital Library

[16]

Russell Impagliazzo and Jan Krajíček. 2002. A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly 48 (2002), 375--377.

[17]

Russell Impagliazzo and Nathan Segerlind. 2001. Counting axioms do not polynomially simulate counting gates. In Proceedings of FOCS 2001. IEEE, 200--209.

Digital Library

[18]

Russell Impagliazzo and Nathan Segerlind. 2006. Constant-depth frege systems with counting axioms polynomially simulate nullstellensatz refutations. ACM Transactions on Computational Logic 7, 2 (2006), 199--218.

Digital Library

[19]

Dmitry Itsykson and Dmitry Sokolov. 2014. Lower bounds for splittings by linear combinations. In Proceedings of MFCS 2014, Part II, E. Csuhaj-Varjú, M. Dietzfelbinger, and Z. Ésik (Eds.). Lecture Notes in Computer Science, Vol. 8635. Springer, 372--383.

[20]

Jan Krajíček. 1994. Lower bounds to the size of constant-depth propositional proofs. The Journal of Symbolic Logic 59, 1 (1994), 73--86.

Digital Library

[21]

J. Krajíček. 1995. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press.

Digital Library

[22]

Jan Krajíček. 1997. Lower bounds for a proof system with an exponential speed-up over constant-depth frege systems and over polynomial calculus. In Proceedings of MFCS ’97, Lecture Notes in Computer Science, Vol. 1295. Springer, 85--90.

Digital Library

[23]

Jan Krajíček. 2016. Randomized feasible interpolation and monotone circuits with a local oracle. https://arxiv.org/abs/1611.08680.

[24]

Massimo Lauria. 2018. A note about k-DNF resolution. Information Processing Letters 137 (2018), 33--39.

[25]

Alexis Maciel, Phuong Nguyen, and Toniann Pitassi. 2014. Lifting lower bounds for tree-like proofs. Computational Complexity 23, 4 (2014), 585--636.

Digital Library

[26]

Alexis Maciel, Toniann Pitassi, and Alan R. Woods. 2002. A new proof of the weak pigeonhole principle. Journal of Computer and System Sciences 64 (2002), 843--872.

Digital Library

[27]

Ran Raz and Iddo Tzameret. 2008. Resolution over linear equations and multilinear proofs. Annals of Pure and Applied Logic 155, 3 (2008), 194--224.

[28]

A. A. Razborov. 1998. Lower bounds for the polynomial calculus. Computational Complexity 7 (1998), 291--324.

Digital Library

[29]

Nathan Segerlind. 2003. New Separations in Propositional Proof Complexity. Ph.D. Dissertation. University of California, San Diego.

Digital Library

[30]

P. M. Spira. 1971. On time hardware complexity tradeoffs for boolean functions. In Proceedings of the 4th Hawaii International Symposium on System Sciences. Western Periodicals Company, North Hollywood, CA, 525--527.

[31]

Gunnar Stålmarck. 1996. Short resolution proofs for a sequence of tricky formulas. Acta Informatica 33, 3 (1996), 277--280.

Digital Library

Cited By

Gryaznov SOvcharov SRiazanov A(2024)Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and SpaceACM Transactions on Computation Theory10.1145/367541516:3(1-15)Online publication date: 11-Jul-2024
https://dl.acm.org/doi/10.1145/3675415
Efremenko KGarlík MItsykson DMohar BShinkar IO'Donnell R(2024)Lower Bounds for Regular Resolution over ParitiesProceedings of the 56th Annual ACM Symposium on Theory of Computing10.1145/3618260.3649652(640-651)Online publication date: 10-Jun-2024
https://dl.acm.org/doi/10.1145/3618260.3649652
Itsykson DRiazanov A(2021)Proof complexity of natural formulas via communication argumentsProceedings of the 36th Computational Complexity Conference10.4230/LIPIcs.CCC.2021.3Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2021.3
Show More Cited By

Index Terms

Some Subsystems of Constant-Depth Frege with Parity
1. Theory of computation
  1. Computational complexity and cryptography
    1. Proof complexity
  2. Logic
    1. Proof theory

Recommendations

Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations

We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m. Central to this is a new definition of reducibility from propositional formulas to systems of polynomials. Using our ...
Poly-logarithmic Frege depth lower bounds via an expander switching lemma
STOC '16: Proceedings of the forty-eighth annual ACM symposium on Theory of Computing

We show that any polynomial-size Frege refutation of a certain linear-size unsatisfiable 3-CNF formula over n variables must have depth Ω(√logn). This is an exponential improvement over the previous best results (Pitassi et al. 1993, Krajíček et al. ...
Parameterized Bounded-Depth Frege Is not Optimal

A general framework for parameterized proof complexity was introduced by Dantchev et al. [2007]. There, the authors show important results on tree-like Parameterized Resolution---a parameterized version of classical Resolution---and their gap complexity ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 19, Issue 4

October 2018

277 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3293495

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 November 2018

Accepted: 01 July 2018

Revised: 01 July 2018

Received: 01 May 2017

Published in TOCL Volume 19, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Polish National Science Centre
European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program
ERC Advanced
ERCIM Alain Bensoussan Fellowship Programme

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
97
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gryaznov SOvcharov SRiazanov A(2024)Resolution Over Linear Equations: Combinatorial Games for Tree-like Size and SpaceACM Transactions on Computation Theory10.1145/367541516:3(1-15)Online publication date: 11-Jul-2024
https://dl.acm.org/doi/10.1145/3675415
Efremenko KGarlík MItsykson DMohar BShinkar IO'Donnell R(2024)Lower Bounds for Regular Resolution over ParitiesProceedings of the 56th Annual ACM Symposium on Theory of Computing10.1145/3618260.3649652(640-651)Online publication date: 10-Jun-2024
https://dl.acm.org/doi/10.1145/3618260.3649652
Itsykson DRiazanov A(2021)Proof complexity of natural formulas via communication argumentsProceedings of the 36th Computational Complexity Conference10.4230/LIPIcs.CCC.2021.3Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2021.3
Part FTzameret I(2021)Resolution with Counting: Dag-Like Lower Bounds and Different Modulicomputational complexity10.1007/s00037-020-00202-x30:1Online publication date: 8-Jan-2021
https://doi.org/10.1007/s00037-020-00202-x
Sokolov DMakarychev KMakarychev YTulsiani MKamath GChuzhoy J(2020)(Semi)Algebraic proofs over {±1} variablesProceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing10.1145/3357713.3384288(78-90)Online publication date: 22-Jun-2020
https://dl.acm.org/doi/10.1145/3357713.3384288
Itsykson DSokolov D(2020)Resolution over linear equations modulo twoAnnals of Pure and Applied Logic10.1016/j.apal.2019.102722171:1(102722)Online publication date: Jan-2020
https://doi.org/10.1016/j.apal.2019.102722
Gryaznov S(2019)Notes on Resolution over Linear EquationsComputer Science – Theory and Applications10.1007/978-3-030-19955-5_15(168-179)Online publication date: 1-Jul-2019
https://dl.acm.org/doi/10.1007/978-3-030-19955-5_15
Itsykson DKnop A(2017)Hard Satisfiable Formulas for Splittings by Linear CombinationsTheory and Applications of Satisfiability Testing – SAT 201710.1007/978-3-319-66263-3_4(53-61)Online publication date: 9-Aug-2017
https://doi.org/10.1007/978-3-319-66263-3_4

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents