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 31 articles )

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

1 2 next

  1. Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF (2019)
  2. Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
  3. van der Hallen, Matthias; Paramonov, Sergey; Janssens, Gerda; Denecker, Marc: Knowledge representation analysis of graph mining (2019)
  4. Lonsing, Florian; Egly, Uwe: (\textsfQRAT^+): generalizing QRAT by a more powerful QBF redundancy property (2018)
  5. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  6. Kiesl, Benjamin; Heule, Marijn J. H.; Seidl, Martina: A little blocked literal goes a long way (2017)
  7. Balabanov, Valeriy; Jiang, Jie-Hong Roland; Scholl, Christoph; Mishchenko, Alan; Brayton, Robert K.: 2QBF: challenges and solutions (2016)
  8. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  9. Janota, Mikoláš: On Q-resolution and CDCL QBF solving (2016)
  10. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  11. Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
  12. Wimmer, Karina; Wimmer, Ralf; Scholl, Christoph; Becker, Bernd: Skolem functions for DQBF (2016)
  13. Fichte, Johannes K.; Szeider, Stefan: Backdoors to normality for disjunctive logic programs (2015)
  14. Finkbeiner, Bernd: Bounded synthesis for Petri games (2015)
  15. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  16. Lonsing, Florian; Egly, Uwe: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API (2015)
  17. Wimmer, Ralf; Gitina, Karina; Nist, Jennifer; Scholl, Christoph; Becker, Bernd: Preprocessing for DQBF ralf (2015)
  18. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: A unified proof system for QBF preprocessing (2014)
  19. Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina: (\mathsfMPIDepQBF): towards parallel QBF solving without knowledge sharing (2014)
  20. Lonsing, Florian; Egly, Uwe: Incremental QBF solving by DepQBF (2014)

1 2 next