QCIR Fuzzer


QCIR 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.


Download qcir-fzuzz as executable jar or the sources.

Run qcir-fuzz with:

java -jar qcir-fuzz.jar m n

  • m: number of universals
  • n: number of existentials



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.