Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable. (English) Zbl 1348.03056
Summary: We show that Level-ordered \(Q\)-resolution and Tree-like \(Q\)-resolution, two restrictions of the \(Q\)-resolution system for proving false QBFs false, are incomparable. While the \(\forall\mathsf{Exp}+\mathsf{Res}\) system is known to \(p\)-simulate Tree-like \(Q\)-resolution, we observe that it cannot \(p\)-simulate Level-ordered \(Q\)-resolution.
Software:
RAReQSReferences:
| [1] | Kleine Büning, H.; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inf. Comput., 117, 12-18 (1995) · Zbl 0828.68045 |
| [2] | Janota, M.; Marques-Silva, J., On propositional QBF expansions and \(Q\)-resolution, (Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing. Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing, SAT, Helsinki, Finland, July 8-12, vol. 7962 (2013)), 67-82 · Zbl 1390.03017 |
| [3] | Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E. M., Solving QBF with counterexample guided refinement, (Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing. Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, Trento, Italy, June 17-20 (2012)), 114-128 · Zbl 1273.68178 |
| [4] | Cadoli, M.; Giovanardi, A.; Schaerf, M., An algorithm to evaluate quantified Boolean formulae, (Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference. Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI, Madison, Wisconsin, USA, July 26-30 (1998)), 262-267 |
| [5] | Cadoli, M.; Schaerf, M.; Giovanardi, A.; Giovanardi, M., An algorithm to evaluate quantified Boolean formulae and its experimental evaluation, J. Autom. Reason., 28, 2, 101-142 (2002) · Zbl 1002.68165 |
| [6] | Janota, M.; Marques-Silva, J., \( \forall Exp + Res\) does not p-simulate \(Q\)-resolution, (International Workshop on Quantified Boolean Formulas (2013)), 17-21 |
| [7] | Janota, M.; Marques-Silva, J., Expansion-based QBF solving versus Q-resolution, Theor. Comput. Sci., 577, 25-42 (2015) · Zbl 1309.68168 |
| [8] | Beyersdorff, O.; Chew, L.; Janota, M., Proof complexity of resolution-based QBF calculi, (32nd International Symposium on Theoretical Aspects of Computer Science. 32nd International Symposium on Theoretical Aspects of Computer Science, STACS (2015)), 76-89, full version in ECCC TR-2014/120 · Zbl 1355.68105 |
| [9] | Bonet, M. L.; Esteban, J. L.; Galesi, N.; Johannsen, J., On the relative complexity of resolution refinements and cutting planes proof systems, SIAM J. Comput., 30, 5, 1462-1484 (2000) · Zbl 0976.03062 |
| [11] | Buresh-Oppenheim, J.; Pitassi, T., The complexity of resolution refinements, J. Symb. Log., 72, 4, 1336-1352 (2007) · Zbl 1160.03005 |
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.
