Concepedia

DepQBF: A Dependency-Aware QBF Solver

Journal on Satisfiability Boolean Modeling and Computation · 2010 · 135 citations · 10 references

Open access

Concepts

ComputingComputer ScienceAlgorithmsLogicAutomated ReasoningBoolean AlgebraDependency ParsingFirst-order LogicPredicate LogicBoolean SatisfiabilityConjunctive Normal FormDependency GraphsDependency Knowledge GraphsEnhanced Dependency GraphsQuantifier Elimination

Abstract

We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQB

References

10

Chaff

Matthew W. Moskewicz, Conor Madigan, Ying Zhao et al. · 2001 · 2.9K citations

Computing, Computer Science, Algorithms +12

BerkMin: A fast and robust SAT-solver

E. Goldberg, Yakov Novikov · Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition · 2003 · 332 citations

Computing, Computer Engineering, Computer Science +7

Resolution for Quantified Boolean Formulas

Hans Kleine Büning, Marek Karpiński, Andreas Flögel · Information and Computation · 1995 · 320 citations

Humanities, Computer Science, Mathematics +9

Chaff: engineering an efficient SAT solver

M.W. Moskewicz, C.F. Madigan, Youpeng Zhao et al. · Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232) · 2002 · 283 citations

Computing, Computer Science, Algorithms +13

An algorithm to evaluate quantified Boolean formulae

Marco Cadoli, Andrea Giovanardi, Marco Schaerf · 1998 · 126 citations

Computing, Computer Science, Algorithms +15