The Equivalences of Refutational QRAT

摘要

The solving of Quantified Boolean Formulas (QBF) has been advanced considerably in the last two decades. In response to this, several proof systems have been put forward to universally verify QBF solvers. QRAT by Heule et al. is one such example of this and builds on technology from DRAT, a checking format used in propositional logic. Recent advances have shown conditional optimality results for QBF systems that use extension variables. Since QRAT can simulate Extended Q-Resolution, we know it is strong, but we do not know if QRAT has the strategy extraction property as Extended Q-Resolution does. In this paper, we partially answer this question by showing that QRAT with a restricted reduction rule has strategy extraction (and consequentially is equivalent to Extended Q-Resolution modulo NP). We also extend equivalence to another system, as we show an augmented version of QRAT known as QRAT+, developed by Lonsing and Egly, is in fact equivalent to the basic QRAT. We achieve this by constructing a line-wise simulation of QRAT+ using only steps valid in QRAT.