DepQBF
swMATH ID: | 9734 |
Software Authors: | Lonsing, F.; Biere, A. |
Description: | 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. |
Homepage: | http://fmv.jku.at/depqbf/ |
Source Code: | https://github.com/lonsing/depqbf |
Related Software: | RAReQS; Bloqqer; Quaffle; MiniSat; sQueezeBF; CAQE; QESTO; HQSpre; semprop; Nenofex; Quantor; QUBOS; QUBE; sKizzo; Chaff; Clingo; QRATPre+; QBFLIB; MPIDepQBF; DRAT-trim |
Cited in: | 57 Documents |
all
top 5
Cited by 94 Authors
all
top 5
Cited in 10 Serials
all
top 5