Quantor
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”.
Keywords for this software
References in zbMATH (referenced in 22 articles , 1 standard article )
Showing results 1 to 20 of 22.
Sorted by year (- Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
- Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
- Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
- Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
- Wimmer, Ralf; Scholl, Christoph; Wimmer, Karina; Becker, Bernd: Dependency schemes for DQBF (2016)
- Wimmer, Ralf; Gitina, Karina; Nist, Jennifer; Scholl, Christoph; Becker, Bernd: Preprocessing for DQBF (2015)
- Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.: Ranking function synthesis for bit-vector relations (2013)
- Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
- Zhou, Conghua; Liu, Zhifeng; Wu, Hailing; Chen, Song; Ju, Shiguang: Symbolic algorithmic verification of intransitive generalized noninterference (2012)
- Biere, Armin; Lonsing, Florian; Seidl, Martina: Blocked clause elimination for QBF (2011)
- Lonsing, Florian; Biere, Armin: Failed literal detection for QBF (2011)
- Egly, Uwe; Seidl, Martina; Woltran, Stefan: A solver for QBFs in negation normal form (2009)
- Goultiaeva, Alexandra; Iverson, Vicki; Bacchus, Fahiem: Beyond CNF: a circuit-based QBF solver (2009)
- Lonsing, Florian; Biere, Armin: A compact representation for syntactic dependencies in QBFs (2009)
- Pulina, Luca; Tacchella, Armando: Learning to integrate deduction and search in reasoning about quantified Boolean formulas (2009)
- Pulina, Luca; Tacchella, Armando: A self-adaptive multi-engine solver for quantified Boolean formulas (2009)
- Samer, Marko; Szeider, Stefan: Backdoor sets of quantified Boolean formulas (2009)
- Stéphan, Igor; Da Mota, Benoit: A unified framework for certificate and compilation for QBF (2009)
- Bubeck, Uwe; Kleine Büning, Hans: Models and quantifier elimination for quantified Horn formulas (2008)
- Gent, Ian P.; Nightingale, Peter; Rowley, Andrew; Stergiou, Kostas: Solving quantified constraint satisfaction problems (2008)