×

A game characterisation of tree-like Q-resolution size. (English) Zbl 1425.03028

Summary: We provide a characterisation for the size of proofs in tree-like Q-Resolution and tree-like QU-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives one of the first successful transfers of one of the lower bound techniques for classical proof systems to QBF proof systems. We apply our technique to show the hardness of three classes of formulas for tree-like Q-Resolution. In particular, we give a proof of the hardness of the parity formulas from [the first two authors et al., LIPIcs – Leibniz Int. Proc. Inform. 30, 76–89 (2015; Zbl 1355.68105)] for tree-like Q-Resolution and of the formulas of H. Kleine Büning et al. [Inf. Comput. 117, No. 1, 12–18 (1995; Zbl 0828.68045)] for tree-like QU-Resolution.

MSC:

03F20 Complexity of proofs
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

Software:

Quaffle; Bloqqer
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Atserias, Albert; Dalmau, Víctor, A combinatorial characterization of resolution width, J. Comput. Syst. Sci., 74, 3, 323-334 (2008) · Zbl 1133.03034
[2] Balabanov, Valeriy; Jiang, Jie-Hong R., Unified QBF certification and its applications, Form. Methods Syst. Des., 41, 1, 45-65 (2012) · Zbl 1284.68516
[3] Balabanov, Valeriy; Widl, Magdalena; Jiang, Jie-Hong R., QBF resolution systems and their proof complexities, (Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT’14) (2014)), 154-169 · Zbl 1423.68406
[4] Beame, Paul; Kautz, Henry A.; Sabharwal, Ashish, Towards understanding and harnessing the potential of clause learning, J. Artif. Intell. Res., 22, 319-351 (2004) · Zbl 1080.68651
[5] Ben-Sasson, Eli; Harsha, Prahladh, Lower bounds for bounded depth Frege proofs via Buss-Pudlák games, ACM Trans. Comput. Log., 11, 3 (2010) · Zbl 1352.03065
[6] Ben-Sasson, Eli; Wigderson, Avi, Short proofs are narrow – resolution made simple, J. ACM, 48, 2, 149-169 (2001) · Zbl 1089.03507
[7] Benedetti, Marco; Mangassarian, Hratch, QBF-based formal verification: experience and perspectives, JSAT, 5, 1-4, 133-191 (2008) · Zbl 1172.68538
[8] Beyersdorff, Olaf; Bonacina, Ilario; Chew, Leroy, Lower bounds: from circuits to QBF proof systems, (Proc. ACM Conference on Innovations in Theoretical Computer Science (ITCS’16) (2016), ACM), 249-260 · Zbl 1334.68084
[9] Beyersdorff, Olaf; Chew, Leroy; Janota, Mikoláš, On unification of QBF resolution-based calculi, (Proc. Symposium on Mathematical Foundations of Computer Science (MFCS’14) (2014), Springer), 81-93 · Zbl 1426.68283
[10] Beyersdorff, Olaf; Chew, Leroy; Janota, Mikoláš, Proof complexity of resolution-based QBF calculi, (Proc. Symposium on Theoretical Aspects of Computer Science (STACS’15) (2015), LIPIcs), 76-89 · Zbl 1355.68105
[11] Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil, Feasible interpolation for QBF resolution calculi, (Proc. International Colloquium on Automata, Languages, and Programming (ICALP’15) (2015), Springer), 180-192 · Zbl 1440.68320
[12] Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil, Are short proofs narrow? QBF resolution is not simple, (Proc. Symposium on Theoretical Aspects of Computer Science (STACS’16) (2016), LIPIcs), 15:1-15:14 · Zbl 1388.03053
[13] Beyersdorff, Olaf; Chew, Leroy; Sreenivasaiah, Karteek, A game characterisation of tree-like Q-resolution size, (Proc. International Conference on Language and Automata Theory and Applications (LATA’15) (2015), Springer), 486-498 · Zbl 1425.03027
[14] 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
[15] Beyersdorff, Olaf; Galesi, Nicola; Lauria, Massimo, A characterization of tree-like resolution size, Inf. Process. Lett., 113, 18, 666-671 (2013) · Zbl 1285.68058
[16] Beyersdorff, Olaf; Galesi, Nicola; Lauria, Massimo, Parameterized complexity of DPLL search procedures, ACM Trans. Comput. Log., 14, 3 (2013) · Zbl 1354.68105
[17] Beyersdorff, Olaf; Kullmann, Oliver, Unified characterisations of resolution hardness measures, (Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT’14) (2014), Springer), 170-187 · Zbl 1423.68409
[18] Beyersdorff, Olaf; Pich, Ján, Understanding Gentzen and Frege systems for QBF, (Proc. ACM/IEEE Symposium on Logic in Computer Science (LICS’16) (2016)) · Zbl 1395.03028
[19] Buss, Samuel R., Towards NP-P via proof complexity and search, Ann. Pure Appl. Logic, 163, 7, 906-917 (2012) · Zbl 1257.03086
[20] Chen, Hubie, Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness, (Proc. International Colloquium on Automata, Languages, and Programming (ICALP’16) (2016)) · Zbl 1387.03067
[21] Cook, Stephen A.; Nguyen, Phuong, Logical Foundations of Proof Complexity (2010), Cambridge University Press · Zbl 1206.03051
[22] Uwe, Egly, On sequent systems and resolution for QBFs, (Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT’12) (2012), Springer), 100-113 · Zbl 1273.03161
[23] Egly, Uwe; Lonsing, Florian; Widl, Magdalena, Long-distance resolution: proof generation and strategy extraction in search-based QBF solving, (Proc. Logic Programming and Automated Reasoning (LPAR’13) (2013)) · Zbl 1406.68106
[24] Esteban, Juan Luis; Torán, Jacobo, A combinatorial characterization of treelike resolution space, Inf. Process. Lett., 87, 6, 295-300 (2003) · Zbl 1161.68637
[25] Goultiaeva, Alexandra; Van Gelder, Allen; Bacchus, Fahiem, A uniform approach for generating proofs and strategies for both true and false QBF formulas, (Proc. International Joint Conference on Artificial Intelligence (IJCAI’11) (2011), Springer), 546-553
[26] Håstad, J., Computational Limitations of Small Depth Circuits (1987), MIT Press: MIT Press Cambridge
[27] Janota, Mikolás, On Q-resolution and CDCL QBF solving, (Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT’16) (2016)), 402-418 · Zbl 1475.68440
[28] Janota, Mikolás; Marques-Silva, Joao, Expansion-based QBF solving versus Q-resolution, Theor. Comput. Sci., 577, 25-42 (2015) · Zbl 1309.68168
[29] Kleine Büning, Hans; Karpinski, Marek; Flögel, Andreas, Resolution for quantified Boolean formulas, Inf. Comput., 117, 1, 12-18 (1995) · Zbl 0828.68045
[30] Krajíček, Jan, Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encycl. Math. Appl., vol. 60 (1995), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0835.03025
[31] Krajíček, Jan, Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic, J. Symb. Log., 62, 2, 457-486 (1997) · Zbl 0891.03029
[32] Laitinen, Tero; Junttila, Tommi A.; Niemelä, Ilkka, Conflict-driven xor-clause learning, (Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT’12) (2012), Springer), 383-396 · Zbl 1273.68322
[33] Lonsing, Florian; Bacchus, Fahiem; Biere, Armin; Egly, Uwe; Seidl, Martina, Enhancing search-based QBF solving by dynamic blocked clause elimination, (Proc. Logic Programming and Automated Reasoning (LPAR’15) (2015)), 418-433 · Zbl 1471.68251
[34] Marques Silva, João P.; Lynce, Inês; Malik, Sharad, Conflict-driven clause learning SAT solvers, (Handbook of Satisfiability. Handbook of Satisfiability, Front. Artif. Intell. Appl., vol. 185 (2009), IOS Press), 131-153
[35] Pudlák, Pavel, Lower bounds for resolution and cutting planes proofs and monotone computations, J. Symb. Log., 62, 3, 981-998 (1997) · Zbl 0945.03086
[36] Pudlák, Pavel, Proofs as games, Am. Math. Mon., 541-550 (2000) · Zbl 0983.03045
[37] Pudlák, Pavel; Buss, Samuel R., How to lie without being (easily) convicted and the length of proofs in propositional calculus, (Proc. Computer Science Logic (CSL’94) (1994)), 151-162 · Zbl 1044.03542
[38] Pudlák, Pavel; Impagliazzo, Russell, A lower bound for DLL algorithms for SAT, (Proc. Symposium on Discrete Algorithms (SODA’00) (2000)), 128-136 · Zbl 0953.68150
[39] Rintanen, Jussi, Asymptotically optimal encodings of conformant planning in QBF, (Proc. Conference on Artificial Intelligence (AAAI’07) (2007), AAAI Press), 1045-1050
[40] Segerlind, Nathan, The complexity of propositional proofs, Bull. Symb. Log., 13, 4, 417-481 (2007) · Zbl 1133.03037
[41] Soos, Mate; Nohl, Karsten; Castelluccia, Claude, Extending SAT solvers to cryptographic problems, (Proc. International Conference on Theory and Applications of Satisfiability Testing SAT’09 (2009), Springer), 244-257
[42] Van Gelder, Allen, Contributions to the theory of practical quantified Boolean formula solving, (Proc. Principles and Practice of Constraint Programming (CP’12) (2012), Springer), 647-663 · Zbl 1390.68585
[43] Zhang, Lintao; Malik, Sharad, Conflict driven learning in a quantified Boolean satisfiability solver, (Proc. IEEE/ACM International Conference on Computer-aided Design (ICCAD’02) (2002)), 442-449 · Zbl 1072.68599
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.