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.


References in zbMATH (referenced in 22 articles )

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

1 2 next

  1. Heule, Marijn J.H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  2. Balabanov, Valeriy; Jiang, Jie-Hong Roland; Scholl, Christoph; Mishchenko, Alan; Brayton, Robert K.: 2QBF: challenges and solutions (2016)
  3. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  4. Janota, Mikoláš: On Q-resolution and CDCL QBF solving (2016)
  5. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  6. Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
  7. Fichte, Johannes K.; Szeider, Stefan: Backdoors to normality for disjunctive logic programs (2015)
  8. Finkbeiner, Bernd: Bounded synthesis for Petri games (2015)
  9. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  10. Lonsing, Florian; Egly, Uwe: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API (2015)
  11. Wimmer, Ralf; Gitina, Karina; Nist, Jennifer; Scholl, Christoph; Becker, Bernd: Preprocessing for DQBF ralf (2015)
  12. Heule, Marijn J.H.; Seidl, Martina; Biere, Armin: A unified proof system for QBF preprocessing (2014)
  13. Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina: $\mathsfMPIDepQBF$: towards parallel QBF solving without knowledge sharing (2014)
  14. Goultiaeva, Alexandra; Bacchus, Fahiem: Recovering and utilizing partial duality in QBF (2013)
  15. Janota, Mikoláš; Marques-Silva, Joao: On propositional QBF expansions and q-resolution (2013)
  16. Lonsing, Florian; Egly, Uwe; Van Gelder, Allen: Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation (2013)
  17. Goultiaeva, Alexandra; Bacchus, Fahiem: Off the trail: re-examining the CDCL algorithm (2012)
  18. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  19. Biere, Armin; Lonsing, Florian; Seidl, Martina: Blocked clause elimination for QBF (2011)
  20. Lonsing, Florian; Biere, Armin: Failed literal detection for QBF (2011)

1 2 next