OVERVIEW ###

OVERVIEW

QRATPre+ is a novel preprocessor to simplify quantified Boolean formulas (QBFs) given in prenex conjunctive normal form (PCNF). For simplification, QRATPre+ tries to eliminate redundant clauses from the PCNF, or universal literals from clauses. It implements redundancy checking based on the QRAT+ proof system. QRAT+ is a generalisation of the QRAT proof system. QRAT was introduced by Heule, Seidl, and Biere:

M. Heule, M. Seidl, A. Biere: Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reasoning 58(1), 2017.
M. Heule, M. Seidl, A. Biere: A Unified Proof System for QBF Preprocessing. JCAR 2014.

QRATPre+ is the first available implementation of the QRAT/QRAT+ proof systems for redundancy removal in QBF preprocessing.

For redundancy checking, the QRAT+ system relies on QBF-specific unit propagation with universal reduction to handle the literals of certain universal variables. This is in contrast to QRAT, which applies propositional unit propagation and treats every variable as existentially quantified. As a result, redundancy removal based on QRAT+ is more powerful than based on QRAT. That strength of QRAT+ is with respect to single applications of rewrite rules. E.g., QRAT+ can remove particular clauses by a single application of a rewrite rule, while QRAT can remove that clause only by applying a sequence of rules.

PUBLICATIONS

A tool paper related to QRATPre+ appeared at SAT 2019:

Florian Lonsing and Uwe Egly. QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. In Proc. of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT) 2019, Springer, LNCS. Preprint: https://arxiv.org/pdf/1904.12927.pdf.

The theory behind QRATPre+ is described in our IJCAR 2018 paper:

Florian Lonsing and Uwe Egly. QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. In Proc. of the 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Springer, LNCS. Preprint: https://arxiv.org/pdf/1804.02908.

QRATPRE+ IN QBFEVAL’18

Runtimes of solvers on 2QBF instances.

The cactus plot above shows the runtimes of the solvers DepQBF-QxQBH, DepQBF-QxBH, and CADET on the instances from the 2QBF track of QBFEVAL 2018. CADET is a state-of-the-art 2QBF solver. DepQBF-QxQBH and DepQBF-QxBH are packages consisting of the QCDCL solver DepQBF and a preprocessing module that integrates several QBF preprocessors. The preprocessing module is implemented as a shell script called QBFRelay. Variant DepQBF-QxQBH includes QRATPre+ whereas variant DepQBF-QxBH does not.

As can be seen from the plot, the use of QRATPre+ in variant DepQBF-QxQBH is crucial to achieve top performance. Thanks to QRATPre+, DepQBF-QxQBH won the 2QBF track in QBFEVAL 2018. While DepQBF-QxQBH solved 275 instances, DepQBF-QxBH solved only 243. It is remarkable that CADET solved 269 without any preprocessing.

Note on practical applications (disclaimer): in contrast to CADET, DepQBF-QxQBH and DepQBF-QxBH do not produce certificates.

SOURCE CODE

QRATPre+ is free software released under GPLv3:

https://www.gnu.org/copyleft/gpl.html

The latest release is available from GitHub.

March 2019: Version 2.0

EXEMPLIFYING THE POWER OF THE QRAT+ SYSTEM

The following examples illustrate that redundancy removal based on QRAT+ as implemented in QRATPre+ is more powerful than based on QRAT, with respect to single applications of rewrite rules. In our implementation, we try to remove clauses and literals by single applications of rewrite rules in multiple rounds. E.g., we do not attempt to remove a clause by applying a sequence of rewrite rules to it within a round.

Clause Elimination

Suppose that we have a file formula.qdimacs containing the following QBF in QDIMACS format:

p cnf 12 14
e 1 2 7 8 0
a 3 9 0
e 4 10 0
a 5 11 0
e 6 12 0
1 3 -4 0
2 -3 4 0
-1 -3 -4 0
-2 3 4 0
3 -4 6 0
-5 -6 0
-1 5 -6 0
7 9 -10 0
8 -9 10 0
-7 -9 -10 0
-8 9 10 0
9 -10 12 0
-11 -12 0
-7 11 -12 0

QRATPre+ is able to remove all clauses in formula.qdimacs. The call ./qratpre+ --print-formula ./formula.qdimacs produces the following output:

p cnf 0 0

Now we configure QRATPre+ to apply redundancy detection based on the QRAT system instead of QRAT+ by parameter --no-eabs. The formula produced by calling ./qratpre+ --print-formula --no-eabs ./formula.qdimacs is exactly the same as the given one, i.e., no redundant clauses can be detected:

p cnf 12 14
e 1 2 7 8 0
a 3 9 0
e 4 10 0
a 5 11 0
e 6 12 0
1 3 -4 0
2 -3 4 0
-1 -3 -4 0
-2 3 4 0
3 -4 6 0
-5 -6 0
-1 5 -6 0
7 9 -10 0
8 -9 10 0
-7 -9 -10 0
-8 9 10 0
9 -10 12 0
-11 -12 0
-7 11 -12 0

Hence clause elimination based on the QRAT+ proof system is more powerful than based on QRAT (see also Proposition 4 in our related IJCAR 2018 paper).

Universal Literal Elimination

Like above, suppose that we have a file formula.qdimacs containing the following QBF in QDIMACS format:

We configure QRATPre+ to only eliminate universal literals by parameters --no-qbce --no-qrate --no-qat, thus switching off clause elimination techniques. QRATPre+ is able to remove all universal variables appearing in the first quantifier block a 1 2 0 from formula.qdimacs. The call ./qratpre+ --print-formula --no-qbce --no-qrate --no-qat ./formula.qdimacs produces the following output:

In contrast to that, if we apply the QRAT system instead of QRAT+ by parameter --no-eabs, then no universal variables can be removed. The formula produced by calling ./qratpre+ --print-formula --no-qbce --no-qrate --no-qat --no-eabs ./formula.qdimacs is exactly the same as the given one:

Hence universal literal elimination based on the QRAT+ proof system is more powerful than based on QRAT with respect to single applications of rewrite rules (see also Proposition 5 in our related IJCAR 2018 paper).

CONTACT INFORMATION

For comments, questions, bug reports etc. related to QRATPre+, please contact:

Florian Lonsing, Stanford University, US

http://www.florianlonsing.com/