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

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

1 2 3 next

  1. Linsbichler, Thomas; Maratea, Marco; Niskanen, Andreas; Wallner, Johannes P.; Woltran, Stefan: Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving (2022)
  2. Sigley, Sarah; Beyersdorff, Olaf: Proof complexity of modal resolution (2022)
  3. Beyersdorff, Olaf; Pulina, Luca; Seidl, Martina; Shukla, Ankit: QBFFam: a tool for generating QBF families from proof complexity (2021)
  4. Bhattacharyya, Arnab; Gupta, Ashutosh; Kuppusamy, Lakshmanan; Mani, Somya; Shukla, Ankit; Srivas, Mandayam; Thattai, Mukund: A formal methods approach to predicting new features of the eukaryotic vesicle traffic system (2021)
  5. Bloem, Roderick; Braud-Santoni, Nicolas; Hadzic, Vedad; Egly, Uwe; Lonsing, Florian; Seidl, Martina: Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations (2021)
  6. Böhm, Benjamin; Beyersdorff, Olaf: Lower bounds for QCDCL via formula gauge (2021)
  7. Chew, Leroy: Hardness and optimality in QBF proof systems modulo NP (2021)
  8. Fandinno, Jorge; Laferriere, Francois; Romero, Javier; Schaub, Torsten; Son, Tran Cao: Planning with incomplete information in quantified answer set programming (2021)
  9. Mengel, Stefan; Slivovsky, Friedrich: Proof complexity of symbolic QBF reasoning (2021)
  10. Beyersdorff, Olaf; Blinkhorn, Joshua; Peitl, Tomáš: Strong (D)QBF dependency schemes via tautology-free resolution paths (2020)
  11. Brewka, Gerhard; Diller, Martin; Heissenberger, Georg; Linsbichler, Thomas; Woltran, Stefan: Solving advanced argumentation problems with answer set programming (2020)
  12. Mayer-Eichberger, Valentin; Saffidine, Abdallah: Positional games and QBF: the corrective encoding (2020)
  13. Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF (2019)
  14. Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
  15. van der Hallen, Matthias; Paramonov, Sergey; Janssens, Gerda; Denecker, Marc: Knowledge representation analysis of graph mining (2019)
  16. Clymo, Judith; Beyersdorff, Olaf: Relating size and width in variants of Q-resolution (2018)
  17. Lonsing, Florian; Egly, Uwe: (\textsfQRAT^+): generalizing QRAT by a more powerful QBF redundancy property (2018)
  18. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  19. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  20. Kiesl, Benjamin; Heule, Marijn J. H.; Seidl, Martina: A little blocked literal goes a long way (2017)

1 2 3 next