This set of scripts serves for generating and presenting instances that should be hard for DPLL-based QBF solvers. QRPCert toolsuite will be needed to reproduce the proofs.

sat13_scripts.tgzp1.qcnf -- Example formula for N=1.

p2.qcnf -- Example formula for N=2.

r1.png -- Example resolution proof for N=1.

r2.png (5.7M) -- Example resolution proof for N=2.

Last updated: Apr 30, 2013 18:10:18