Additional material for the submission: On Propositional QBF Expansions and Q-Resolution

M. Janota, J. Marques-Silva

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.

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