zbMATH — the first resource for mathematics

\({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property. (English) Zbl 06958098
Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-94204-9/pbk; 978-3-319-94205-6/ebook). Lecture Notes in Computer Science 10900. Lecture Notes in Artificial Intelligence, 161-177 (2018).
Summary: The \(\mathsf{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 \(\mathsf{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 \(\mathsf{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 \(\mathsf{QRAT}\) we call \(\mathsf{QRAT}^{+}\). The redundancy property in \(\mathsf{QRAT}^{+}\) based on QUP is more powerful than the one in \(\mathsf{QRAT}\) based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of \(\mathsf{QRAT}^{+}\) for QBF preprocessing.
For the entire collection see [Zbl 1391.68006].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI