QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property

TL;DR

QRAT+ extends the QRAT proof system for QBFs by incorporating a more powerful redundancy check using QBF-specific unit propagation, leading to improved preprocessing capabilities.

Contribution

The paper introduces QRAT+, a generalized QRAT system utilizing QBF-specific unit propagation, enhancing redundancy detection and proof efficiency.

Findings

QRAT+ outperforms QRAT in proof theoretical strength.

QRAT+ improves QBF preprocessing effectiveness.

Experimental results show better redundancy elimination.

Abstract

The QRAT (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning tools. It consists of rules to rewrite a QBF by adding and deleting clauses and universal literals that have a certain redundancy property. To check for this redundancy property in QRAT, propositional unit propagation (UP) is applied to the quantifier free, i.e., propositional part of the QBF. We generalize the redundancy property in the QRAT system by QBF specific UP (QUP). QUP extends UP by the universal reduction operation to eliminate universal literals from clauses. We apply QUP to an abstraction of the QBF where certain universal quantifiers are converted into existential ones. This way, we obtain a generalization of QRAT we call QRAT+. The redundancy property in QRAT+ based on QUP is more powerful than the one in QRAT based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of QRAT+ for QBF preprocessing.