FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property

Authors: Florian Lonsing and Uwe Egly

Paper Information

Title:QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Authors:Florian Lonsing and Uwe Egly
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:quantified Boolean formulas, QBF, proof systems, preprocessing, unit propagation, QRAT, quantified resolution asymmetric tautology
Abstract:

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., purely 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 which we call QRAT+. The resulting 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 on experimental results to illustrate the benefits of using QRAT+ for QBF preprocessing.

Pages:16
Talk:Jul 15 09:00 (Session 101E: SAT)
Paper: