Quantor

Download

Since the initial release of quantor we worked on minor internal improvements. The basic algorithm has not changed except for extracting functional dependencies as also used in SATeLite. Self subsuming resolution does not work correctly in the context of QBF. Both features are described in our paper "Effective Preprocessing in SAT through Variable and Clause Elimination" on SATeLite.

You may want to have a look at the README file, and the installation instructions, contained in the INSTALL file, that come with the sources.

License

With the new source release we moved to a BSD style LICENSE. In essence, you can use the source code and compiled binaries in any way, if you keep the original license in the source code and reproduce it in a binary. Read the full text for more details.

Background

Quantor is a solver for quantified boolean formulas (QBF) in the QDIMACS format. Checking satisfiability of QBF, the QBF problem, is the standard PSPACE complete problem. Many practically important problems, such as non-deterministic planning or symbolic model checking can be formulated succinctly in QBF. In our recent talk at DCC'06 we mention 7 applications.

More information on the QBF problem can be found at QBFLIB. The algorithm behind Quantor is discribed in a paper with the title "Resolve and Expand". It was also used as preprocessor in the context of SAT and as such was submitted to the SAT'04 SAT Solver Competition. This application is described in more detail in our technical report "The Evolution from Limmat to Nanosat".

Old Versions

[ quantor-3.0.tar.gz | quantor-2.11.gz (Linux-x86) | quantor-2004.01.25.gz (Linux-x86) ]

The latter version of Quantor was used for the experiments reported in our SAT'04 paper "Resolve and Expand".