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.

sat13_scripts.tgz
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.

[HOME]


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