
Darwin
 Referenced in 25 articles
[sw04175]
 Model Evolution Calculus lifts the propositional DPLL procedure to firstorder logic ... developed by the SAT community for the DPLL procedure. The current version of Darwin implements...

ManySAT
 Referenced in 32 articles
[sw00544]
 obtained through careful variations of the standard DPLL algorithm. Additionally, each sequential algorithm shares clauses...

DepQBF
 Referenced in 31 articles
[sw09734]
 normal form. It is based on the DPLL algorithm for QBF with conflictdriven clause...

NiVER
 Referenced in 18 articles
[sw06958]
 complexity. To tackle that, the backtrackingbased DPLL procedure [{it M. Davis}, {it G. Logemann ... then solve the simplified problem using a DPLL SAT solver. NiVER is a strictly formula...

HySAT
 Referenced in 24 articles
[sw01980]
 systems, incorporating a tight integration of a DPLLbased pseudoBoolean SAT solver...

sharpSAT
 Referenced in 23 articles
[sw16713]
 that is based on the well known DPLL algorithm and techniques from...

MaxSolver
 Referenced in 20 articles
[sw01990]
 Davis–Putnam–Logemann–Loveland procedure (DPLL) is one of the most competitive exact algorithms...

semprop
 Referenced in 17 articles
[sw28383]
 format implemented in the style of the DPLL procedure. In this paper, socalled learning...

BarcelogicTools
 Referenced in 9 articles
[sw02001]
 efficient implementation of the DPLL(T) framework [Ganzingeretal2004CAV, Nieuwenhuisetal2005LPAR]. A DPLL(T) system consists ... general DPLL(X) engine, very similar in nature to a SAT solver, whose parameter ... solver for a theory T. Once the DPLL(X) engine has been implemented, this approach...

DPvis
 Referenced in 7 articles
[sw00219]
 instances and runs of the DPLL (DavisPutnamLogemannLoveland) procedure. DPvis uses advanced graph ... problem’s structure during a typical DPLL run. Besides implementing a simple variant ... DPLL algorithm on its own, DPvis also features an interface to MiniSAT, a state ... DPLL implementation. Using this interface, runs of MiniSAT can be visualized  including the generated search...

MathCheck
 Referenced in 10 articles
[sw13642]
 input conjecture (just like the T in DPLL(T)). In addition, the combination enables...

Lynx
 Referenced in 10 articles
[sw13643]
 literature and in the context of DPLL(T), it has not been previously made available...

CirCUs
 Referenced in 9 articles
[sw00128]
 solve by traditional solvers based on DPLL...

kcnfs
 Referenced in 8 articles
[sw00484]
 kcnfs is a dpll based solver. kcnfs integrates a branching variable heuristic devoted essentially...

QingTing1
 Referenced in 7 articles
[sw04452]
 search and other stateoftheart DPLLbased SAT solvers. The resulting comparisons show...

NAGSAT
 Referenced in 4 articles
[sw11453]
 solution of 3SAT instances using the DPLL Algorithm and outline some of our current...

QMiraXT
 Referenced in 4 articles
[sw11456]
 QMiraXT  A multithreaded QBF solver. Dieser DPLL suchbasierte Solver ist eine Erweiterung des multi...

satUZK
 Referenced in 4 articles
[sw18570]
 easily extendable. In addition to the standard DPLL [1] algorithm with clause learning the solver...

IsaFoL
 Referenced in 4 articles
[sw19193]
 ground and firstorder calculi, such as DPLL, CDCL, and resolution. One of our inspirations...