DepQBF is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form. It is based on the DPLL algorithm for QBF with conflict-driven clause and solution-driven cube learning. By analyzing the structure of a formula, DepQBF tries to identify independent variables. In addition to other benefits, this often increases freedom for decision making. See also the JSAT system description of DepQBF 0.1 from QBFEVAL’10 for references and a brief outline of the idea. DepQBF 0.1 participated in QBFEVAL’10. See the competition website for performance results. For bug reports etc., please contact Florian Lonsing.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
- Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
- Lonsing, Florian; Egly, Uwe: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API (2015)
- Heule, Marijn J.H.; Seidl, Martina; Biere, Armin: A unified proof system for QBF preprocessing (2014)
- Goultiaeva, Alexandra; Bacchus, Fahiem: Recovering and utilizing partial duality in QBF (2013)
- Janota, Mikoláš; Marques-Silva, Joao: On propositional QBF expansions and q-resolution (2013)
- Lonsing, Florian; Egly, Uwe; Van Gelder, Allen: Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation (2013)
- Goultiaeva, Alexandra; Bacchus, Fahiem: Off the trail: re-examining the CDCL algorithm (2012)
- Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
- Lonsing, Florian; Biere, Armin: Integrating dependency schemes in search-based QBF solvers (2010)