View on GitHub

QRATPre+

A preprocessor for quantified Boolean formulas.

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:

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.

PUBLICATIONS

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

A preprint of the above paper is available on arXiv:

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.

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.

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 (i.e., a formula with a quantifier prefix but not containing any clauses):

p cnf 12 0
e 1 2 7 8 0
a 3 9 0
e 4 10 0
a 5 11 0
e 6 12 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 using the QRAT system:

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:

p cnf 6 8
a 1 2 0
e 3 4 0
a 5 0
e 6 0
-2 -3 -4 0
-1 -3 4 0
1 3 -4 0
2 3 4 0
-3 -4 6 0
5 -6 0
-3 4 -6 0
-5 6 0

We configure QRATPre+ to only eliminate universal literals by parameters --no-qbce --no-qrate --no-at, 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-at ./formula.qdimacs produces the following output (the quantifier prefix is not cleaned up):

p cnf 6 8
a 1 2 0
e 3 4 0
a 5 0
e 6 0
-3 -4 0
-3 4 0
3 -4 0
3 4 0
-3 -4 6 0
5 -6 0
-3 4 -6 0
-5 6 0

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-at --no-eabs ./formula.qdimacs is exactly the same as the given one:

p cnf 6 8
a 1 2 0
e 3 4 0
a 5 0
e 6 0
-2 -3 -4 0
-1 -3 4 0
1 3 -4 0
2 3 4 0
-3 -4 6 0
5 -6 0
-3 4 -6 0
-5 6 0

Hence universal literal elimination based on the QRAT+ proof system is more powerful than based on QRAT (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, TU Wien, Austria

http://www.kr.tuwien.ac.at/staff/lonsing/