CirQit
CirQit is a non-CNF QBF solver that uses a circuit representation.
It is based on a prototype originally developed by Vicky Iverson, it has since been rewritten and
expanded by Alexandra Goultiaeva under the supervision of
Fahiem Bacchus.
Its most notable new feature is dual propagation, which allows
solving both the problem and its negation at the same time.
CirQit2.1 has solved the most problems in the non-prenex non-CNF track of
QBFEval'10.
Download
The following downloads are available for free for non-commertial use. Might be buggy, use at your own risk.
The documentation is poor, but please contact me if you need help/explanations!
I am also interested in non-CNF problems, so if you're working on some instances you're willing to share,
I'd be happy to have them!
(Nov 2012) CirQit3.1.7a, and its source code.
Fixes a bug where an assertion checks guarbage memory. Most of the time the memory happens to be non-0,
and the assertion passes. However, this seems to fail on a MAC. Thanks to Wei Yang Tan for bringing this to me!
Some scripts for dealing with certificates in version 3.
CirQit3.1.7: A new version of CirQit as of 2011. It includes the ability to generate
certificates, and has command line options to switch between reading iscas, qpro and qdimacs.
Be warned, CirQit does need the non-CNF structure to be efficient. Do not expect good performance when feeding it qdimacs.
Source code of CirQit3.1.7: Messy and undocumented, sorry! Feel free to email
for explanations.
qbf2iscas: A converter from prenex QBF1.0 to ISCAS by Vicky Iverson. Takes one argument (the QBF1.0 file),
dumps the output to standard out. Source file here.
CirQit2.1: A statically linked ELF-32 executable for Linux. This file was submitted to
QBFEval'10 and uses the same conventions for input and output.