team
contact
software
publications
teaching
jobs

QCIR Fuzzer

Overview

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.

Downloads

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

Experiments

1000 instances for m=1000 and n=40, n=45, n=50
Runtimes of RAReQS and ghostQ

Publication

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.