DepQBF

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

Anything in here will be replaced on browsers that support the canvas element


References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  2. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  3. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  4. Lonsing, Florian; Egly, Uwe: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API (2015)
  5. Heule, Marijn J.H.; Seidl, Martina; Biere, Armin: A unified proof system for QBF preprocessing (2014)
  6. Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina: $\mathsfMPIDepQBF$: towards parallel QBF solving without knowledge sharing (2014)
  7. Goultiaeva, Alexandra; Bacchus, Fahiem: Recovering and utilizing partial duality in QBF (2013)
  8. Janota, Mikoláš; Marques-Silva, Joao: On propositional QBF expansions and q-resolution (2013)
  9. Lonsing, Florian; Egly, Uwe; Van Gelder, Allen: Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation (2013)
  10. Goultiaeva, Alexandra; Bacchus, Fahiem: Off the trail: re-examining the CDCL algorithm (2012)
  11. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  12. Lonsing, Florian; Biere, Armin: Integrating dependency schemes in search-based QBF solvers (2010)
  13. Lonsing, Florian; Biere, Armin: DepQBF: A dependency-aware QBF solver (2010)