sKizzo - a QBF solver

sKizzo is a solver for deciding Quantified Boolean Formulas (QBFs). It is designed to tell formulas having at least one model from those having none.

For example, you can exploit sKizzo to decide that the following statement:

UNSAT QBF formula

has no model (it is "unsatisfiable") while this one:

SAT QBF formula

has at least one model (it is "satisfiable").

The decision of QBFs has relevant practical applications. Techniques do exist to translate planning problems, model checking problems, and many others into QBF instances. Formulas arising from such applications may contain tens of quantifier alternations, thousands of variables and millions of clauses.

sKizzo was in development from 2004-2011. It had several notable features and records; namely, it was the first solver to:

exploit skolemization to solve quantified propositional formulas;
extract certificates of satisfiability from true formulas;
employ symbolic variants of the common QBF inference rules;
feature a hybrid inference engine that merged resolution-based preprocessing, DPLL-like search, SAT-based reasoning, symbolic inferences, and abstract branching;
reconstruct quantifier trees out of prenex linear DIMACS inputs in order to exploit them in all the aforementioned inference engines;
implement the first QBF decision procedure wholly different from resolution, expansion, or DPLL-like search (abstract branching);
be able to deal with (a limited form of) restricted quantifiers in the input;
enumerate all valid assignments to (the outermost scope of) any true formula.

Back then, sKizzo was one of the strongest solvers available; on many families of QBF instances - especially those from formal verification - it was the reference solver: It won two of the three international QBF competitions in which it took part (2005, 2006, and 2007).

Underlying all these results is the (then novel) concept of symblic skolemization, a technique that blends binary decision digrams (BDDs) and conjunctive normal form formulas (CNF) to represent and reason on QBF instances. You find documents describing this technique and the internals of sKizzo in the "Documentation" section below.

Don't hesitate to drop me a line if you want to know more.

sKizzo is implemented in C/C++. Source code is not available at present but will be at some point. Notable releases are/were:

sKizzo v0.1, the first complete implementation, used for the experimental evaluation in the tech. rep. TR04-11-03 (see below) [August 2004].
sKizzo v0.5, a largely improved version, which participated in the QBF05 evaluation. Rev. 77 [March 2005].
sKizzo v0.6, the first publically available version. Released as rev. 151 [May 2005].
sKizzo v0.8.2, released as rev. 3XX, is the most widely circulated release [March 2006].
sKizzo v0.9, version for the QBF06 competition. Not available publically [June 2006].
sKizzo v0.12, latest version publically available; includes solution enumeration and restricted quantifiers [March 2011].

The model reconstructor/certifier/inspector ozziKs is also publically available.
Major steps in this implementation are:

ozziKs v0.1: The first implementation (not public), used for the experimental evaluation in the IJCAI05 paper (see below). Rev. 52 [January 2005].
ozziKs v0.2: The first full-featured version, distributed upnon request, rev. 206 [August 2005].
ozziKs v0.3: The first version available here. Released as rev. 393 [November 2006].

Current version (v0.12) relies on the following libraries:

The zChaff SAT solver, version 2004.5.13, for ground reasoning.
The minisat SAT solver, version 1.14, for ground reasoning.
The CUDD package, version 2.4.0, for BDD manipulation.
The DDDMP package, version 2.0.3, for BDD load and store.

All such libraries are statically linked with the solver (and acknowledged as required), so you need nothing more than the solver itself to be up and running.

Some experimental results (mostly outdated):

Some quantifier trees extracted out of flat prenex instances in the QBFLIB are reported. Downloadable PDF and DOT formats are given.
Some experimental results reporting the time taken and the amount of memory necessary to solve non-random benchmarks in the QBFLIB.
Some experimental results reporting the time taken to verify the answers of the solver, and to extract a certificate of satisfiability (SAT instances) or an unsatisfiable core (UNSAT instances).

Papers describing some aspects of sKizzo:

Hratch Mangassarian, Andreas G. Veneris, Marco Benedetti: Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test. IEEE Trans. Computers 59(7): 981-994 (2010) [PDF, BibTex]
Marco Benedetti and Hratch Mangassarian, Experience and Perspectives in QBF-Based Formal Verification, JSAT 5(1-4): 133-191 (2008) [PDF, BibTex]
Marco Benedetti, Arnaud Lallouet, and Jérémie Vautard, QCSP made Practical by virtue of Restricted Quantification, in Proc. of 10th International Joint Conference on Artificial Intelligence (IJCAI07), 2007 [PDF, BibTex]
Marco Benedetti, Abstract Branching for Quantified Formulas, in Proc. of 21st National Conference on Artificial Intelligence (AAAI06), 2006 [PDF, BibTex]
Marco Benedetti, sKizzo: a Suite to Evaluate and Certify QBFs, in Proc. of 20th International Conference on Automated Deduction (CADE05), 2005 [PDF, BibTex]
Marco Benedetti, Hybrid Evaluation Procedures for QBFs, in Intelligenza Artificiale, 2005
Marco Benedetti, Extracting Certificates from Quantified Boolean Formulas, in Proc. of 9th International Joint Conference on Artificial Intelligence (IJCAI05), 2005 [PDF, BibTex]
Marco Benedetti, Evaluating QBFs via Symbolic Skolemization, in Proc. of 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR04), n. 3452 in LNCS, Springer, 2005 [PDF, BibTex]
Marco Benedetti, Quantifier Trees for QBFs, in Proc. of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT05), 2005 [PDF (extended version), BibTex]

Technical/Unpublished Reports:

Marco Benedetti, Symbolically Quantified Propositional Logic (SQPL), Unpubliched manuscript, November 2007 [PDF]
Marco Benedetti, sKizzo: a QBF decision procedure based on Propositional Skolemization and Symbolic Reasoning, Tech. Rep. TR04-11-03, ITC-Irst, November 2004 [PDF, BibTex]

User manuals: