On Tseitin formulas, read-once branching programs and treewidth. (English) Zbl 1517.68091
van Bevern, René (ed.) et al., Computer science – theory and applications. 14th international computer science symposium in Russia, CSR 2019, Novosibirsk, Russia, July 1–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11532, 143-155 (2019).
Summary: We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an \(n\times n\) grid graph has size at least \(2^{\varOmega (n)}\). Then using the Excluded Grid theorem by Robertson and Seymour we show that for arbitrary graph \(G(V, E)\) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on \(G\) has size at least \(2^{\varOmega (\operatorname{tw}(G)^\delta )}\) for all \(\delta <1/36\), where \(\operatorname{tw}(G)\) is the treewidth of \(G\) (for planar graphs and some other classes of graphs the statement holds for \(\delta =1)\). We also show an upper bound of \(O(|E| 2^{\operatorname{pw}(G)})\), where \(\operatorname{pw}(G)\) is the pathwidth of \(G\).
We apply the mentioned results to the analysis of the complexity of derivations in the proof system \(\mathrm{OBDD}(\land, \mathrm{reordering})\) and show that any \(\mathrm{OBDD}(\land, \mathrm{reordering})\)-refutation of an unsatisfiable Tseitin formula based on a graph \(G\) has size at least \(2^{\varOmega (\operatorname{tw}(G)^\delta )}\).
For the entire collection see [Zbl 1416.68013].
We apply the mentioned results to the analysis of the complexity of derivations in the proof system \(\mathrm{OBDD}(\land, \mathrm{reordering})\) and show that any \(\mathrm{OBDD}(\land, \mathrm{reordering})\)-refutation of an unsatisfiable Tseitin formula based on a graph \(G\) has size at least \(2^{\varOmega (\operatorname{tw}(G)^\delta )}\).
For the entire collection see [Zbl 1416.68013].
MSC:
| 68P05 | Data structures |
| 03F20 | Complexity of proofs |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68R10 | Graph theory (including graph drawing) in computer science |
References:
| [1] | Alekhnovich, M.; Razborov, AA, Satisfiability, branch-width and tseitin tautologies, Comput. Complex., 20, 4, 649-678, 2011 · Zbl 1243.68182 · doi:10.1007/s00037-011-0033-1 |
| [2] | Atserias, A.; Kolaitis, PG; Vardi, MY; Wallace, M., Constraint propagation as a proof system, Principles and Practice of Constraint Programming - CP 2004, 77-91, 2004, Heidelberg: Springer, Heidelberg · Zbl 1152.68537 · doi:10.1007/978-3-540-30201-8_9 |
| [3] | Buss, S., Itsykson, D., Knop, A., Sokolov, D.: Reordering rule makes OBDD proof systems stronger. In: CCC-2018, pp. 16:1-16:24 (2018) · Zbl 1441.03042 |
| [4] | Chekuri, C.; Chuzhoy, J., Polynomial bounds for the grid-minor theorem, J. ACM, 63, 5, 40:1-40:65, 2016 · Zbl 1410.05186 · doi:10.1145/2820609 |
| [5] | Chuzhoy, J.: Excluded grid theorem: improved and simplified. In: Proceedings of STOC-2015, pp. 645-654 (2015) · Zbl 1321.05248 |
| [6] | Dantchev, S.S., Riis, S.: “planar” tautologies hard for resolution. In: FOCS-2001, pp. 220-229 (2001) |
| [7] | Ferrara, A.; Pan, G.; Vardi, MY; Sutcliffe, G.; Voronkov, A., Treewidth in verification: local vs. global, Logic for Programming, Artificial Intelligence, and Reasoning, 489-503, 2005, Heidelberg: Springer, Heidelberg · Zbl 1143.68450 · doi:10.1007/11591191_34 |
| [8] | Galesi, N.; Talebanfard, N.; Torán, J.; Beyersdorff, O.; Wintersteiger, CM, Cops-robber games and the resolution of Tseitin formulas, Theory and Applications of Satisfiability Testing - SAT 2018, 311-326, 2018, Cham: Springer, Cham · Zbl 1499.03054 · doi:10.1007/978-3-319-94144-8_19 |
| [9] | Glinskih, L., Itsykson, D.: Satisfiable Tseitin formulas are hard for nondeterministic read-once branching programs. In: MFCS-2017, pp. 26:1-26:12 (2017) · Zbl 1441.68156 |
| [10] | Glinskih, L., Itsykson, D.: On Tseitin formulas, read-once branching programs and treewidth. Technical Reports. TR-19-020, ECCC (2019) |
| [11] | Gu, QP; Tamaki, H., Improved bounds on the planar branchwidth with respect to the largest grid minor size, Algorithmica, 64, 3, 416-453, 2012 · Zbl 1257.05028 · doi:10.1007/s00453-012-9627-5 |
| [12] | Håstad, J.: On small-depth Frege proofs for Tseitin for grids. In: FOCS-2017, pp. 97-108 (2017) |
| [13] | Itsykson, D., Knop, A., Romashchenko, A., Sokolov, D.: On OBDD-based algorithms and proof systems that dynamically change order of variables. In: STACS-2017, pp. 43:1-43:14 (2017) · Zbl 1402.68097 |
| [14] | Korach, E.; Solel, N., Tree-width, path-width, and cutwidth, Discrete Appl. Math., 43, 1, 97-101, 1993 · Zbl 0788.05057 · doi:10.1016/0166-218X(93)90171-J |
| [15] | Krajíček, J., Bounded Arithmetic, Propositional Logic and Complexity Theory, 1995, Cambridge: Cambridge University Press, Cambridge · Zbl 0835.03025 · doi:10.1017/CBO9780511529948 |
| [16] | Lovász, L.; Naor, M.; Newman, I.; Wigderson, A., Search problems in the decision tree model, SIAM J. Discrete Math., 8, 1, 119-132, 1995 · Zbl 0817.68112 · doi:10.1137/S0895480192233867 |
| [17] | Razgon, I., On the read-once property of branching programs and CNFs of bounded treewidth, Algorithmica, 75, 2, 277-294, 2016 · Zbl 1350.68156 · doi:10.1007/s00453-015-0059-x |
| [18] | Robertson, N.; Seymour, P.; Thomas, R., Quickly excluding a planar graph, J. Comb. Theory Ser. B, 62, 2, 323-348, 1994 · Zbl 0807.05023 · doi:10.1006/jctb.1994.1073 |
| [19] | Robertson, N.; Seymour, PD, Graph minors. V. Excluding a planar graph, J. Comb. Theory Ser. B, 41, 1, 92-114, 1986 · Zbl 0598.05055 · doi:10.1016/0095-8956(86)90030-4 |
| [20] | Tseitin, GS, On the complexity of derivation in the propositional calculus, Zapiski nauchnykh seminarov LOMI, 8, 234-259, 1968 · Zbl 0197.00102 |
| [21] | Urquhart, A., Hard examples for resolution, JACM, 34, 1, 209-219, 1987 · Zbl 0639.68093 · doi:10.1145/7531.8928 |
| [22] | Wegener, I., Branching Programs and Binary Decision Diagrams, 2000, Philadelphia: SIAM, Philadelphia · Zbl 0956.68068 · doi:10.1137/1.9780898719789 |
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.
