Term-resolution provides an elegant mechanism to prove that a quantified Boolean formula (QBF) is true. It is a dual to Q-resolution and is practically highly important as it enables certifying answers of DPLL-based QBF solvers. While term-resolution and Q-resolution are very similar, they are not completely symmetrical. In particular, Q-resolution operates on clauses and term-resolution operates on models of the matrix. This paper investigates the impact of this asymmetry. We will see that there is a large class of formulas (formulas with “big models”) whose term-resolution proofs are exponential. As a possible remedy, the paper suggests to prove true QBFs by refuting their negation (negate-refute), rather than proving them by term-resolution. The paper shows that from the theoretical perspective this is indeed a favorable approach. In particular, negation-refutation p-simulates term-resolution and there is an exponential separation between the two calculi. These observations further our understanding of proof systems for QBFs and provide a strong theoretical underpinning for the effort towards non-CNF QBF solvers.
CITATION STYLE
Janota, M., & Marques-Silva, J. (2017). An Achilles’ Heel of term-resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10423 LNAI, pp. 670–680). Springer Verlag. https://doi.org/10.1007/978-3-319-65340-2_55
Mendeley helps you to discover research relevant for your work.