Ooq - A CNF-reconstructing Dual solver

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 following downloads are available for free for non-commertial use. Might be buggy, use at your own risk.

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!

  • Ooq 0.0 Beta (statically linked 64-bit) WARNING: !known bug! This version does not correctly handle input problems which contain clauses with repeated or complimentary literals.
  • Usage:

    To use:
    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 definition
    If 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).
    The formula reconstructor ONLY to get statistics about the formula:
    Reconstruction statistics: A statically linked binary .