Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6876055 | Theoretical Computer Science | 2015 | 18 Pages |
Abstract
This article introduces and studies a proof system âExp+Res that enables us to refute quantified Boolean formulas (QBFs). The system âExp+Res operates in two stages: it expands all universal variables through conjunctions and refutes the result by propositional resolution. This approach contrasts with the Q-resolution calculus, which enables refuting QBFs by rules similar to propositional resolution. In practice, Q-resolution enables producing proofs from conflict-driven DPLL-based QBF solvers. The system âExp+Res can on the other hand certify certain expansion-based solvers. So a natural question is to ask which of the systems, Q-resolution and âExp+Res, is more powerful? The article gives several partial responses to this question. On the positive side, we show that âExp+Res can p-simulate tree Q-resolution. On the negative side, we show that âExp+Res does not p-simulate unrestricted Q-resolution. In the favor of âExp+Res we show that âExp+Res is more powerful than a certain fragment of Q-resolution, which is important for DPLL-based QBF solving.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
MikoláÅ¡ Janota, Joao Marques-Silva,