a b c d e f g h i j k l m n o p q r s t u v w x y z
Description: solver for quantified boolean formulae
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, called QDPLL, with conflict-driven clause and solution-driven
cube learning. By analyzing the syntactic structure of a formula,
DepQBF tries to identify independent variables. In general, information
on independent variables can be represented in the formal framework of
dependency schemes. DepQBF computes the so-called "standard dependency
scheme" of a given formula. In addition to other benefits, information
on independent variables often increases the freedom for decision
making and clause learning.
Description: solver for quantified boolean formulae
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.
--- 133189 Thu Jan 1 00:00:00 1970
+++ 86647 Thu Jan 1 00:00:00 1970
@@ -1,11 +1,7 @@
solver for quantified boolean formulae
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, called QDPLL, with conflict-driven clause and solution-driven
+ for QBF with conflict-driven clause and solution-driven cube
- cube learning. By analyzing the syntactic structure of a formula,
+ learning. By analyzing the structure of a formula, DepQBF tries to
- DepQBF tries to identify independent variables. In general, information
+ identify independent variables. In addition to other benefits, this
- on independent variables can be represented in the formal framework of
+ often increases freedom for decision making.
- dependency schemes. DepQBF computes the so-called "standard dependency
- scheme" of a given formula. In addition to other benefits, information
- on independent variables often increases the freedom for decision
- making and clause learning.