• Darwin

  • Referenced in 25 articles [sw04175]
  • Model Evolution Calculus lifts the propositional DPLL procedure to first-order 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 conflict-driven clause...
  • NiVER

  • Referenced in 18 articles [sw06958]
  • complexity. To tackle that, the backtracking-based 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 DPLL-based pseudo-Boolean 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, so-called 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 (Davis-Putnam-Logemann-Loveland) 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 state-of-the-art DPLL-based SAT solvers. The resulting comparisons show...
  • NAGSAT

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

  • Referenced in 4 articles [sw11456]
  • QMiraXT - A multithreaded QBF solver. Dieser DPLL such-basierte 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 first-order calculi, such as DPLL, CDCL, and resolution. One of our inspirations...