 |
|
|
 | |
 |
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:
has no model (it is "unsatisfiable") while this one:
has at least one model (it is "satisfiable").
Apart from being an important theorical problem by itself, the decision of QBFs has relevant practical applications.
For example, techniques do exist to translate planning problems and unbounded model checking problems for discrete dynamic systems into QBF instances.
Unfortunately, formulas arising from such applications are not as small as shown in the examples above.
They may indeed contain tens of quantifier alternations, thousands of variables and millions of clauses.
|
| |
 |
sKizzo is based on a new technique, called symbolic skolemization, and on a related
form of symbolic reasoning. This approach makes it differ from all the previous QBF solvers.
Symbolic skolemization and reasoning exploit binary decision digrams (BDDs) to represent and manage instances.
As opposed to previous BDD-based approaches (like the ones in QBDD or ZQSAT)
sKizzo's leverages a two-level data structure tailored to quantified formulas, and designed to take advantage of their structure.
On top of these building blocks a hybrid inference engine is employed.
It augments the native, symbolic-skolemization based inference style of the solver with the following additional reasoning styles:
- bottom-up resolution-based techniques
(extending the approach of Biere [SAT04] implemented in quantor)
- top-down DPLL-like reasoning (like in Cadoli, Giovanardi, Schaerf [AAAI-98], and improvements thereof),
- SAT-based reasoning (somehow related to what QUBOS does).
You find documents describing the internals of sKizzo in the "Download" section below. Don't hesitate to drop me a line if you want to know more.
|
| |
 |
sKizzo features a beta-quality C implementation (object-oriented programming style, developed on Xcode 1.2/1.5, compiled with gcc 4.0, profiled with Shark 4.0).
Major steps in this implementation are:
- sKizzo v0.1, the first complete implementation (not public), used for the experimental evaluation in the tech. rep. TR04-11-03 (see below). August 2004.
- sKizzo v0.5, a largely improved version (not public), which participated in the QBF05 evaluation. Rev. 77, March 2005.
- sKizzo v0.6, the first publically available version. Released on May 2, 2005 as rev. 151.
- sKizzo v0.8.2: The latest available version. Released on March 15, 2006 as rev. 3XX.
- sKizzo v0.9: Version for the QBF06 competition. Not available publically. February 2006.
- sKizzo v0.10, upcoming public release.
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 on request between August 2005 and November 2006, rev. 206.
- ozziKs v0.3: The first version available here. Released on November 10, 2006 as rev. 393.
Current version (v0.8.2) 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.
|
| |
 |
Even if sKizzo is work-in-progress, we put a lot of effort into obtaining an updated performance profile for the solver.
Results are divided into three categories:
-
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:
- 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, to appear, 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 Reports:
- 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:
- sKizzo v0.8-beta, User Manual, v0.4 for revision 257
[PDF]
- ozziKs v0.3-beta, User Manual, v0.2 for revision 393
[PDF]
|
| |
 |
| Software |
Supported Platforms |
sKizzo:
The QBF solver. |
|
|
|
ozziKs:
A companion application to manipulate sat-certificates. |
|
|
|
libsK:
A library with a C API to load and query certificates (models). |
[not yet] |
[net yot] |
[not yet] |
qTree:
An application to experiment with quantifier trees. |
|
|
[no] |
|
| |
 |
The best source of information for QBF instances and solvers is the QBF library, maintained by the University of Genova.
There you'll find (at least) a lot of random and non-random QBF instances, a list of people involved in QBF and a list of known QBF solvers.
Also, a session devoted to QBF is held in the SAT series of conferences (and reported in the proceedings thereof).
Since a couple of years, a QBF solver evaluation session takes place takes place during such conferences.
|
