×

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

Dediu, Adrian-Horia (ed.) et al., Language and automata theory and applications. 9th international conference, LATA 2015, Nice, France, March 2–6, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8977, 486-498 (2015).
Summary: We provide a characterisation for the size of proofs in tree-like Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution [the first author et al., Inf. Process. Lett. 113, No. 18, 666–671 (2013; Zbl 1285.68058)]. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF proof systems. We confirm our technique with two previously known hard examples. In particular, we give a proof of the hardness of the formulas of H. Kleine Büning et al. [Inf. Comput. 117, No. 1, 12–18 (1995; Zbl 0828.68045)] for tree-like Q-Resolution.
For the entire collection see [Zbl 1331.68009].

MSC:

03F20 Complexity of proofs
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Atserias, A.; Dalmau, V., A combinatorial characterization of resolution width, Journal of Computer and System Sciences, 74, 3, 323-334 (2008) · Zbl 1133.03034 · doi:10.1016/j.jcss.2007.06.025
[2] Balabanov, V.; Jiang, J-HR, Unified QBF certification and its applications, Formal Methods in System Design, 41, 1, 45-65 (2012) · Zbl 1284.68516 · doi:10.1007/s10703-012-0152-6
[3] Balabanov, V.; Widl, M.; Jiang, J-HR; Sinz, C.; Egly, U., QBF resolution systems and their proof complexities, Theory and Applications of Satisfiability Testing - SAT 2014, 154-169 (2014), Heidelberg: Springer, Heidelberg · Zbl 1423.68406 · doi:10.1007/978-3-319-09284-3_12
[4] Ben-Sasson, E., Harsha, P.,: Lower bounds for bounded depth Frege proofs via Buss-Pudlák games. ACM Trans. on Computational Logic 11(3) (2010) · Zbl 1352.03065
[5] Ben-Sasson, E.; Wigderson, A., Short proofs are narrow - resolution made simple, Journal of the ACM, 48, 2, 149-169 (2001) · Zbl 1089.03507 · doi:10.1145/375827.375835
[6] Benedetti, M.; Mangassarian, H., QBF-based formal verification: Experience and perspectives, JSAT, 5, 1-4, 133-191 (2008) · Zbl 1172.68538
[7] Beyersdorff, O.; Chew, L.; Janota, M.; Csuhaj-Varjú, E.; Dietzfelbinger, M.; Ésik, Z., On unification of QBF resolution-based calculi, Mathematical Foundations of Computer Science 2014, 81-93 (2014), Heidelberg: Springer, Heidelberg · Zbl 1426.68283 · doi:10.1007/978-3-662-44465-8_8
[8] Beyersdorff, O.; Chew, L.; Janota, M., Proof complexity of resolution-based QBF calculi, ECCC, 21, 120 (2014)
[9] Beyersdorff, O.; Galesi, N.; Lauria, M., A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games, Information Processing Letters, 110, 23, 1074-1077 (2010) · Zbl 1379.03017 · doi:10.1016/j.ipl.2010.09.007
[10] Beyersdorff, O.; Galesi, N.; Lauria, M., A characterization of tree-like resolution size, Information Processing Letters, 113, 18, 666-671 (2013) · Zbl 1285.68058 · doi:10.1016/j.ipl.2013.06.002
[11] Beyersdorff, O., Galesi, N., Lauria, M.,: Parameterized complexity of DPLL search procedures. ACM Trans. on Computational Logic 14(3) (2013) · Zbl 1354.68105
[12] Beyersdorff, O.; Kullmann, O.; Sinz, C.; Egly, U., Unified characterisations of resolution hardness measures, Theory and Applications of Satisfiability Testing - SAT 2014, 170-187 (2014), Heidelberg: Springer, Heidelberg · Zbl 1423.68409 · doi:10.1007/978-3-319-09284-3_13
[13] Buss, SR, Towards NP-P via proof complexity and search, Ann. Pure Appl. Logic, 163, 7, 906-917 (2012) · Zbl 1257.03086 · doi:10.1016/j.apal.2011.09.009
[14] Cook, S.A., Nguyen, P.: Logical Foundations of Proof Complexity. Cambridge University Press (2010) · Zbl 1206.03051
[15] Egly, U.; Cimatti, A.; Sebastiani, R., On sequent systems and resolution for QBFs, Theory and Applications of Satisfiability Testing - SAT 2012, 100-113 (2012), Heidelberg: Springer, Heidelberg · Zbl 1273.03161 · doi:10.1007/978-3-642-31612-8_9
[16] Egly, U.; Lonsing, F.; Widl, M.; McMillan, K.; Middeldorp, A.; Voronkov, A., Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving, Logic for Programming, Artificial Intelligence, and Reasoning, 291-308 (2013), Heidelberg: Springer, Heidelberg · Zbl 1406.68106 · doi:10.1007/978-3-642-45221-5_21
[17] Esteban, JL; Torán, J., A combinatorial characterization of treelike resolution space, Information Processing Letters, 87, 6, 295-300 (2003) · Zbl 1161.68637 · doi:10.1016/S0020-0190(03)00345-4
[18] Janota, M., Marques-Silva, J.: \( \forall\) Exp+Res does not p-simulate Q-resolution. International Workshop on Quantified Boolean Formulas (2013)
[19] Janota, M.; Marques-Silva, J.; Järvisalo, M.; Van Gelder, A., On propositional QBF expansions and Q-resolution, Theory and Applications of Satisfiability Testing - SAT 2013, 67-82 (2013), Heidelberg: Springer, Heidelberg · Zbl 1390.03017 · doi:10.1007/978-3-642-39071-5_7
[20] Büning, HK; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inf. Comput., 117, 1, 12-18 (1995) · Zbl 0828.68045 · doi:10.1006/inco.1995.1025
[21] Krajíček, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory (1995), Cambridge: Cambridge University Press, Cambridge · Zbl 0835.03025 · doi:10.1017/CBO9780511529948
[22] Krajíček, J., Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic, J. Symb. Log., 62, 2, 457-486 (1997) · Zbl 0891.03029 · doi:10.2307/2275541
[23] Pudlák, P.: Proofs as games. American Math. Monthly, pp. 541-550 (2000) · Zbl 0983.03045
[24] Pudlák, P., Impagliazzo, R.: A lower bound for DLL algorithms for SAT. In: Proc. 11th Symposium on Discrete Algorithms, pp. 128-136 (2000) · Zbl 0953.68150
[25] Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: AAAI, pp. 1045-1050. AAAI Press, (2007)
[26] Segerlind, N., The complexity of propositional proofs, Bulletin of Symbolic Logic, 13, 4, 417-481 (2007) · Zbl 1133.03037 · doi:10.2178/bsl/1203350879
[27] Van Gelder, A.: Contributions to the theory of practical quantified Boolean formula solving. In: CP, pp. 647-663 (2012) · Zbl 1390.68585
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.