×

Quantor

swMATH ID: 28381
Software Authors: Biere, Armin
Description: Quantor: 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. 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”.
Homepage: http://fmv.jku.at/quantor/
Related Software: sKizzo; QUBOS; DepQBF; Bloqqer; MiniSat; QUBE; sQueezeBF; PicoSAT; Nenofex; QuBE++; QBFLIB; semprop; Quaffle; CAQE; Easychair; NiVER; z3; CirQit2; C4.5; Lingeling
Cited in: 22 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Resolve and expand. Zbl 1122.68585
Biere, Armin
2005

Citations by Year