QCIR-to-QDIMACS converter

The QCIR format supports QBFs in circuit form. There are a growing number of QBF solvers that can read QCIR directly and profitably make use of the circuit structure. However, many existing QBF solvers work only on QDIMACS, countering the usefulness of QCIR as a target format for those who wish to encode QBF problems. To remedy this situation, we provide a conversion script qcir-to-qdimacs.py that takes prenex QCIR as input and translates it to QDIMACS. Non-prenex QCIR is not currently supported by this tool.

Download: qcir-to-qdimacs.py

Usage: python qcir-to-qdimacs.py input.qcir -o output.qdimacs

For the opposite direction, to try to reverse-engineer QCIR from QDIMACS, see qcir-conv.py from GhostQ.

Example:

Input: fig1.qcir Output: fig1.qdimacs



#QCIR-G14
forall(v1)
exists(v2, v3)
output(g3)
g1 = and(v1, v2)
g2 = and(-v1, -v2, v3)
g3 = or(g1, g2)

c VarName   1 : v1
c VarName   2 : v2
c VarName   3 : v3
p cnf 6 11
a 1  0
e 2 3 4 5 6  0
6  0
4 -1 -2  0
-4 1  0
-4 2  0
5 1 2 -3  0
-5 -1  0
-5 -2  0
-5 3  0
-6 4 5  0
6 -4  0
6 -5  0

Note about the VarName lines: The converter tries to preserve the names of input and gate variables. However, if it cannot do so for an input variable (either because the variable name is not a positive integer or because it is larger than the number of variables), then it produces a VarName line that records what number the variable has been mapped to. This can be turned off with the "--keep-var-names 0" option.