OverviewQCIR is a gate-based input format for quantified Boolean formulas in non-PCNF.
Our tool qcir-fuzz is a random generator producing QCIR formulas according to the fixed shape model with a forall-exists prefix.
DownloadsDownload qcir-fzuzz as executable jar or the sources.
Run qcir-fuzz with:
java -jar qcir-fuzz.jar m n
The experiments are described in our paper Non-CNF QBF Solving with QCIR accepted for the AAAI-16 Workshop on Beyond NP.
Errata: In the paper, the random model is described by |X| = n and |Y| = m, but it should be |X| = m and |Y| = n.