Ooq is a CNF-based QBF solver. Beyond the standard CDCL features it is equipped with the ability to perform partial dual propagation on the structure it discovers in the CNF.
The idea of using dual propagtion in a CNF-based solver is described here:
Goultiaeva, A, Seidl, M and Biere, A. Bridging the gap between dual propagation and CNF-based QBF solving. DATE'2013: 811-814
Partial dual propagation is described in this paper:
Goultiaeva, A and Bacchus, F. Recovering and Utilizing Partial Duality in QBF. SAT'13
The solver is not well-documented, but feel free to contact me if you need help!
The documentation is poor, but please contact me if you need help/explanations!
Also let me know if you find problems!
Note: to get the actual dual propagation, use the parameter "-e" (see below for usage details)
Note2: currently the "magic" is hidden inside the solver; it takes standard qdimacs.
I plan to make it compatible with other reconstruction/generation methods.
I'd be glad to hear from you if you have
thoughts on a good format for that, and/or applications and/or reconstruction algorithms!
oooq <problem_file> [flag] [-stats]
- <problem_file> is the QDIMACS problem
- [flag] is one of the following:
-eg expand gates
-ei expand implications
-e expand both
- Using the option "-stats" turns off solving.
the solver will attempt reconstruction,
print statistics, and exit.
The problem statistics are:
Variables: the number of variables after introducing duals InitClauses: the number of clauses in the problem InitCubes: the number of "seeding" cubes created RemainingClauses: the number of clauses that were NOT a part of some definition vars forced: the number of variables whose value was forced by unit clauses vars pure: the number of variables initially pure vars gated: the number of variables linked to a gate definition (AND and OR gates) vars implied: the number of variables linked to an implication definition vars equiv: the number of variables linked to an equivalence definitionIf a field is empty, it is 0. To see if your formula has been well reconstructed, compare InitClauses and RemainingClauses. If RemainingClauses is 0 or 1, then all the structure has been reconstructed. (it is 0 if the output clause is unit). If RemainingClauses is -1, then you haven't turned on dual propagation (option "-e", see above).