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.68585Biere, Armin 2005 all top 5 Cited by 43 Authors 6 Biere, Armin 4 Lonsing, Florian 4 Seidl, Martina 2 Becker, Bernd 2 Egly, Uwe 2 Pulina, Luca 2 Scholl, Christoph 2 Tacchella, Armando 2 Wimmer, Ralf D. 2 Wintersteiger, Christoph M. 1 Bacchus, Fahiem 1 Bubeck, Uwe 1 Chen, Song 1 Cook, Byron 1 da Mota, Benoit 1 de Moura, Leonardo 1 Eén, Niklas 1 Gent, Ian Philip 1 Gitina, Karina 1 Goultiaeva, Alexandra 1 Hamadi, Youssef 1 Heule, Marijn J. H. 1 Iverson, Vicki 1 Ju, Shiguang 1 Khasidashvili, Zurab O. 1 Kleine Büning, Hans 1 Korovin, Konstantin 1 Kröning, Daniel 1 Liu, Zhifeng 1 Nightingale, Peter W. 1 Nist, Jennifer 1 Rabe, Markus N. 1 Rowley, Andrew G. D. 1 Rümmer, Philipp 1 Samer, Marko 1 Seshia, Sanjit Arunkumar 1 Stéphan, Igor 1 Stergiou, Kostas 1 Szeider, Stefan 1 Wimmer, Karina 1 Woltran, Stefan 1 Wu, Hailing 1 Zhou, Conghua all top 5 Cited in 6 Serials 2 Journal of Automated Reasoning 2 Formal Methods in System Design 2 Constraints 1 Artificial Intelligence 1 Discrete Applied Mathematics 1 Science China. Information Sciences Cited in 3 Fields 22 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year