QBF Solver

[SSoelvsten]

We had earlier a crude and quite bad SAT solver. We should redo it from the ground up as a QBF solver (where SAT is a special case of having no explicit quantification and only free variables).

• Construct qcir circuit from file.
  • Derive the level of each gate
  • Derive the desired Variable Ordering
    • INPUT/MATRIX: The order they are defined (as per the cleansed order). This is essentially the order they are defined in the matrix.
    • QUANT: The order as they defined in the quantification block.
    • DFS: The first occurence of a variable's leaf in a depth-first traversal of the matrix.
    • LEVEL: Based on the deepest depth a variable occurs within the circuit. Ties are broken with DFS.
  • Support free variables by adding an existential gate at the top.
• Compute the decision diagram for the formula by recursing through the qcir circuit. The circuit itself probably can be implemented quite similarly to Picotrav.
  • Bottom-up evaluate the circuit (similar to Picotrav); i.e. compute the evaluation order of the levels in the circuit.
  • The top-most quantifier block is not solved with BDDs, but rather a witness/counter-example is extracted from the BDD.