Bounded-depth Frege complexity of Tseitin formulas for all graphs. (English) Zbl 1516.03021
The article is well organized and written. The preliminaries section is very well written.
The article is a contribution to the complexity of proofs in bounded-depth Frege proving new bounds for Tseitin formulas.
The main result comes from the application of J. Håstad’s [J. ACM 68, No. 1, Paper No. 1, 31 p. (2021; Zbl 1499.03056)] result on small-depth Frege proofs for Tseitin for grids, which is an improve of [T. Pitassi et al., in: Proceedings of the 48th annual ACM SIGACT symposium on theory of computing, STOC ’16, Cambridge, MA, USA, June 19–21, 2016. New York, NY: Association for Computing Machinery (ACM). 644–657 (2016; Zbl 1373.03125)] of super-polynomial bounded-depth Frege refutations of Tseiting fromulas over expander graphs, the authors prove tight bounds (lower and upper) on the size of refutations in bounded-depth Frege of \(T(G,f)\) over any graph \(G\) in terms of the treewidth of \(G\). More precisely, in Section 3, the authors prove the lower bound such that, first they show that if \(H\) is a topological minor of \(G\), then any bounded-depth Frege proof of \(\neg T(G,f)\) can be transformed to a proof of \(\neg T(H,f^\prime)\), with constant increase in depth and polynomial in size. And then, they prove a lower bound on the size of depth-\(d\) Frege proof of \(\neg T(H,f^\prime)\) base on walls and using Håstad’s result [loc. cit.], in short the bound is at least \({2^{tw(G)}}^{{\Omega}(\frac{1}{d})}\).
In Section 4, the authors prove the upper bound, for this goal, they use the compact representation of CNF linear functions, and the derivations from linear equations, that is, because, Tseitin formula is an unsatisfiable system of CNF linear equations and finally, they use the treewidth of \(G\) considering D. R. Wood’s [Eur. J. Comb. 30, No. 5, 1245–1253 (2009; Zbl 1205.05079)] result on tree-partition of a graph \(G\), proving that the upper bound is at most \({2^{tw(G)}}^{\mathcal{O}(\frac{1}{d})} \mathrm{poly}(|T(G,f)|)\).
As a consequence of the main results, in Section 5, the authors show that if \(T(G,f)\) has a refutation of size \(S\) in bounded-depth Frege, then it has a refutation of size at most \(2^{\mathrm{poly}(\log S)}\) in treelike resolution and vice versa, providing evidence of quasi-polynomial size related to A. Urquhart’s conjecture [J. Assoc. Comput. Mach. 34, 209–219 (1987; Zbl 0639.68093)].
Finally, they settle the question posed by M. Alekhnovich and A. Razborov [Comput. Complexity 20, No. 4, 649–678 (2011; Zbl 1243.68182)] of showing the class of Tseitin formulas is quasi-automatizable for resolution for any quasi-smooth graph.
There is a typo on page 2 line 17, say ‘ans’ must be ‘and’.
The article is a contribution to the complexity of proofs in bounded-depth Frege proving new bounds for Tseitin formulas.
The main result comes from the application of J. Håstad’s [J. ACM 68, No. 1, Paper No. 1, 31 p. (2021; Zbl 1499.03056)] result on small-depth Frege proofs for Tseitin for grids, which is an improve of [T. Pitassi et al., in: Proceedings of the 48th annual ACM SIGACT symposium on theory of computing, STOC ’16, Cambridge, MA, USA, June 19–21, 2016. New York, NY: Association for Computing Machinery (ACM). 644–657 (2016; Zbl 1373.03125)] of super-polynomial bounded-depth Frege refutations of Tseiting fromulas over expander graphs, the authors prove tight bounds (lower and upper) on the size of refutations in bounded-depth Frege of \(T(G,f)\) over any graph \(G\) in terms of the treewidth of \(G\). More precisely, in Section 3, the authors prove the lower bound such that, first they show that if \(H\) is a topological minor of \(G\), then any bounded-depth Frege proof of \(\neg T(G,f)\) can be transformed to a proof of \(\neg T(H,f^\prime)\), with constant increase in depth and polynomial in size. And then, they prove a lower bound on the size of depth-\(d\) Frege proof of \(\neg T(H,f^\prime)\) base on walls and using Håstad’s result [loc. cit.], in short the bound is at least \({2^{tw(G)}}^{{\Omega}(\frac{1}{d})}\).
In Section 4, the authors prove the upper bound, for this goal, they use the compact representation of CNF linear functions, and the derivations from linear equations, that is, because, Tseitin formula is an unsatisfiable system of CNF linear equations and finally, they use the treewidth of \(G\) considering D. R. Wood’s [Eur. J. Comb. 30, No. 5, 1245–1253 (2009; Zbl 1205.05079)] result on tree-partition of a graph \(G\), proving that the upper bound is at most \({2^{tw(G)}}^{\mathcal{O}(\frac{1}{d})} \mathrm{poly}(|T(G,f)|)\).
As a consequence of the main results, in Section 5, the authors show that if \(T(G,f)\) has a refutation of size \(S\) in bounded-depth Frege, then it has a refutation of size at most \(2^{\mathrm{poly}(\log S)}\) in treelike resolution and vice versa, providing evidence of quasi-polynomial size related to A. Urquhart’s conjecture [J. Assoc. Comput. Mach. 34, 209–219 (1987; Zbl 0639.68093)].
Finally, they settle the question posed by M. Alekhnovich and A. Razborov [Comput. Complexity 20, No. 4, 649–678 (2011; Zbl 1243.68182)] of showing the class of Tseitin formulas is quasi-automatizable for resolution for any quasi-smooth graph.
There is a typo on page 2 line 17, say ‘ans’ must be ‘and’.
Reviewer: Ariel Germán Fernández (Buenos Aires)
MSC:
| 03F20 | Complexity of proofs |
| 05C83 | Graph minors |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Ajtai, Miklós, The complexity of the pigeonhole principle, Combinatorica, 14, 4, 417-433 (1994) · Zbl 0811.03042 |
| [2] | Alekhnovich, Michael; Razborov, Alexander A., Resolution is not automatizable unless W[P] is tractable, SIAM J. Comput., 38, 4, 1347-1363 (2008) · Zbl 1169.03044 |
| [3] | Alekhnovich, Michael; Razborov, Alexander A., Satisfiability, branch-width and Tseitin tautologies, Comput. Complex., 20, 4, 649-678 (2011) · Zbl 1243.68182 |
| [4] | Atserias, Albert; Müller, Moritz, Automating resolution is NP-hard, J. ACM, 67, 5, 31:1-31:17 (2020) · Zbl 1491.68078 |
| [5] | Beame, Paul; Beck, Chris; Impagliazzo, Russell, Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space, SIAM J. Comput., 45, 4, 1612-1645 (2016) · Zbl 1401.68094 |
| [6] | Beame, Paul; Pitassi, Toniann, Simplified and improved resolution lower bounds, (37th Annual Symposium on Foundations of Computer Science, FOCS’96, 14-16 October, 1996 (1996), IEEE Computer Society: IEEE Computer Society Burlington, Vermont, USA), 274-282 · Zbl 0866.03029 |
| [7] | Bellantoni, Stephen; Pitassi, Toniann; Urquhart, Alasdair, Approximation and small-depth Frege proofs, SIAM J. Comput., 21, 6, 1161-1179 (1992) · Zbl 0762.03020 |
| [8] | Belmonte, Rémy; Giannopoulou, Archontia; Lokshtanov, Daniel; Thilikos, Dimitrios M., The structure of \(w_4\)-immersion-free graphs, (ICGT 2014 (2016)) |
| [9] | Ben-Sasson, Eli, Hard examples for the bounded depth Frege proof system, Comput. Complex., 11, 3-4, 109-136 (2002) · Zbl 1043.03043 |
| [10] | Ben-Sasson, Eli; Wigderson, Avi, Short proofs are narrow - resolution made simple, J. ACM, 48, 2, 149-169 (2001) · Zbl 1089.03507 |
| [11] | Beyersdorff, Olaf; Galesi, Nicola; Lauria, Massimo, A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games, Inf. Process. Lett., 110, 23, 1074-1077 (2010) · Zbl 1379.03017 |
| [12] | Buss, Samuel R., Polynomial size proofs of the propositional pigeonhole principle, J. Symb. Log., 52, 4, 916-927 (1987) · Zbl 0636.03053 |
| [13] | Chuzhoy, Julia, Excluded grid theorem: improved and simplified, (Servedio, Rocco A.; Rubinfeld, Ronitt, Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing. Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, June 14-17, 2015 (2015), ACM: ACM Portland, OR, USA), 645-654 · Zbl 1321.05248 |
| [14] | Chuzhoy, Julia; Tan, Zihan, Towards tight(er) bounds for the excluded grid theorem, (Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms. Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’19, Philadelphia, PA, USA. Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms. Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’19, Philadelphia, PA, USA, Society for Industrial and Applied Mathematics (2019)), 1445-1464 · Zbl 1434.05146 |
| [15] | Cook, Stephen A.; Reckhow, Robert A., The relative efficiency of propositional proof systems, J. Symb. Log., 44, 1, 36-50 (1979) · Zbl 0408.03044 |
| [16] | Dantchev, Stefan S.; Riis, Søren, Tree resolution proofs of the weak pigeon-hole principle, (Proceedings of the 16th Annual IEEE Conference on Computational Complexity. Proceedings of the 16th Annual IEEE Conference on Computational Complexity, June 18-21, 2001 (2001), IEEE Computer Society: IEEE Computer Society Chicago, Illinois, USA), 69-75 |
| [17] | Davis, Martin; Logemann, George; Loveland, Donald W., A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002 |
| [18] | Davis, Martin; Putnam, Hilary, A computing procedure for quantification theory, J. ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203 |
| [19] | Dvorák, Zdenek; Wollan, Paul, A structure theorem for strong immersions, J. Graph Theory, 83, 2, 152-163 (2016) · Zbl 1346.05279 |
| [20] | Furst, Merrick L.; Saxe, James B.; Sipser, Michael, Parity, circuits, and the polynomial-time hierarchy, Math. Syst. Theory, 17, 1, 13-27 (1984) · Zbl 0534.94008 |
| [21] | Galesi, Nicola; Itsykson, Dmitry; Riazanov, Artur; Sofronova, Anastasia, Bounded-depth frege complexity of tseitin formulas for all graphs, (Rossmanith, Peter; Heggernes, Pinar; Katoen, Joost-Pieter, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany. 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, LIPIcs, vol. 138 (2019), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 49:1-49:15 · Zbl 1539.03187 |
| [22] | Galesi, Nicola; Talebanfard, Navid; Torán, Jacobo, Cops-robber games and the resolution of Tseitin formulas, ACM Trans. Comput. Theory, 12, 2, 9:1-9:22 (2020) · Zbl 1499.03054 |
| [23] | Glinskih, Ludmila; Itsykson, Dmitry, On Tseitin formulas, read-once branching programs and treewidth, Electron. Colloq. Comput. Complex., 26, 20 (2019) · Zbl 1517.68091 |
| [24] | Gu, Qian-Ping; Tamaki, Hisao, Improved bounds on the planar branchwidth with respect to the largest grid minor size, Algorithmica, 64, 3, 416-453 (Nov 2012) · Zbl 1257.05028 |
| [25] | Haken, Armin, The intractability of resolution, Theor. Comput. Sci., 39, 297-308 (1985) · Zbl 0586.03010 |
| [26] | Harvey, Daniel J.; Wood, David R., The treewidth of line graphs, J. Comb. Theory, Ser. B, 132, 157-179 (2018) · Zbl 1391.05218 |
| [27] | Hastad, Johan, Computational Limitations of Small-Depth Circuits (1987), MIT Press |
| [28] | Håstad, Johan, On small-depth Frege proofs for Tseitin for grids, (Umans, Chris, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, October 15-17, 2017 (2017), IEEE Computer Society: IEEE Computer Society Berkeley, CA, USA), 97-108 |
| [29] | Itsykson, Dmitry; Oparin, Vsevolod, Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP, (Bulatov, Andrei A.; Shur, Arseny M., Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings. Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7913 (2013), Springer), 162-173 · Zbl 1381.68098 |
| [30] | Itsykson, Dmitry; Oparin, Vsevolod; Slabodkin, Mikhail; Sokolov, Dmitry, Tight lower bounds on the resolution complexity of perfect matching principles, Fundam. Inform., 145, 3, 229-242 (2016) · Zbl 1432.03117 |
| [31] | Itsykson, Dmitry; Riazanov, Artur; Sagunov, Danil; Smirnov, Petr, Almost tight lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs, Comput. Complex., 30, 2, 13 (2021) · Zbl 1497.03066 |
| [32] | Jukna, Stasys, Boolean Function Complexity: Advances and Frontiers (2012), Springer · Zbl 1235.94005 |
| [33] | Krajícek, Jan; Pudlák, Pavel; Woods, Alan R., An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Struct. Algorithms, 7, 1, 15-40 (1995) · Zbl 0843.03032 |
| [34] | Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell, Exponential lower bounds for the pigeonhole principle, Comput. Complex., 3, 97-140 (1993) · Zbl 0784.03034 |
| [35] | Pitassi, Toniann; Rossman, Benjamin; Servedio, Rocco A.; Tan, Li-Yang, Poly-logarithmic Frege depth lower bounds via an expander switching lemma, (Wichs, Daniel; Mansour, Yishay, Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing. Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, June 18-21, 2016 (2016), ACM: ACM Cambridge, MA, USA), 644-657 · Zbl 1373.03125 |
| [36] | Pudlák, Pavel; Buss, Samuel R., How to lie without being (easily) convicted and the lengths of proofs in propositional calculus, (Pacholski, Leszek; Tiuryn, Jerzy, Computer Science Logic (1995), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 151-162 · Zbl 1044.03542 |
| [37] | Raz, Ran, Resolution lower bounds for the weak pigeonhole principle, J. ACM, 51, 2, 115-138 (2004) · Zbl 1317.03036 |
| [38] | Razborov, Alexander A., Lower bounds on the size of bounded depth networks over a complete basis with logical addition, Mat. Zametki, 41, 598-607 (1987) · Zbl 0632.94030 |
| [39] | Razborov, Alexander A., Resolution lower bounds for the weak functional pigeonhole principle, Theor. Comput. Sci., 303, 1, 233-243 (2003) · Zbl 1050.03039 |
| [40] | Razborov, Alexander A., Resolution lower bounds for perfect matching principles, J. Comput. Syst. Sci., 69, 1, 3-27 (2004) · Zbl 1106.03049 |
| [41] | Robertson, Neil; Seymour, Paul; Thomas, Robin, Quickly excluding a planar graph, J. Comb. Theory, Ser. B, 62, 2, 323-348 (1994) · Zbl 0807.05023 |
| [42] | Smolensky, Roman, Algebraic methods in the theory of lower bounds for Boolean circuit complexity, (Aho, Alfred V., Proceedings of the 19th Annual ACM Symposium on Theory of Computing. Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA (1987), ACM: ACM New York, New York, USA), 77-82 |
| [43] | Grigory S. Tseitin, On the complexity of derivation in the propositional calculus, in: A.O. Slisenko (Ed.), Studies in Constructive Mathematics and Mathematical Logic Part II, a968. |
| [44] | Urquhart, Alasdair, Hard examples for resolution, J. ACM, 34, 1, 209-219 (1987) · Zbl 0639.68093 |
| [45] | Urquhart, Alasdair; Fu, Xudong, Simplified lower bounds for propositional proofs, Notre Dame J. Form. Log., 37, 4, 523-544 (1996) · Zbl 0882.03052 |
| [46] | Wood, David R., On tree-partition-width, Part Special Issue on Metric Graph Theory. Part Special Issue on Metric Graph Theory, Eur. J. Comb., 30, 5, 1245-1253 (2009) · Zbl 1205.05079 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
