DPLL algorithm
In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.
- Caption
- enAfter 5 fruitless attempts ', choosing the variable assignment a=1, b=1 leads, after unit propagation ', to success : the top left CNF formula is satisfiable.
- Class
- Boolean satisfiability problem
- Comment
- enIn logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.
- Data
- Binary tree
- Depiction
- Has abstract
- enIn logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. It was introduced in 1961 by Martin Davis, George Logemann and Donald W. Loveland and is a refinement of the earlier Davis–Putnam algorithm, which is a resolution-based procedure developed by Davis and Hilary Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the "Davis–Putnam method" or the "DP algorithm". Other common names that maintain the distinction are DLL and DPLL.
- ImageSize
- 300
- Is primary topic of
- DPLL algorithm
- Label
- enDPLL algorithm
- Link from a Wikipage to an external page
- portal.acm.org/citation.cfm%3Fcoll=GUIDE&dl=GUIDE&id=321034
- archive.org/details/machineprogramfo00davi
- Link from a Wikipage to another Wikipage
- Automated planning and scheduling
- Automated theorem proving
- Backjumping
- Backtracking
- Binary decision diagram
- Binary tree
- Boolean satisfiability problem
- Category:Articles with example pseudocode
- Category:Automated theorem proving
- Category:Constraint programming
- Category:SAT solvers
- Communications of the ACM
- Completeness (logic)
- Computational complexity theory
- Computer science
- Conflict-Driven Clause Learning
- Conjunctive normal form
- Davis–Putnam algorithm
- Diagnosis (artificial intelligence)
- Donald W. Loveland
- DPLL(T)
- First-order logic
- George Logemann
- GRASP (SAT solver)
- Herbrandization
- Heuristic function
- Hilary Putnam
- Implication graph
- Journal of the ACM
- Logic
- Martin Davis (mathematician)
- Mathematical theory
- Model checking
- NP-complete
- Polarity (mathematical logic)
- Proof complexity
- Propositional logic
- Propositional variable
- Resolution (logic)
- Satisfiability modulo theories
- SAT solver
- Search algorithm
- Short-circuiting operator
- Stålmarck's method
- Truth value
- Unit propagation
- ZChaff
- Name
- enDPLL
- SameAs
- Algorithme DPLL
- Algoritmo DPLL
- Algoritmo DPLL
- DPLL
- DPLL
- DPLL algorithm
- DPLL-algoritme
- DPLL алгоритм
- DPLLアルゴリズム
- DPLL算法
- m.080fyp
- Q2030088
- vkUb
- ДПЛЛ алгоритам
- الگوریتم DPLL
- Space
- Subject
- Category:Articles with example pseudocode
- Category:Automated theorem proving
- Category:Constraint programming
- Category:SAT solvers
- Thumbnail
- WasDerivedFrom
- DPLL algorithm?oldid=1094417709&ns=0
- WikiPageLength
- 14433
- Wikipage page ID
- 2745094
- Wikipage revision ID
- 1094417709
- WikiPageUsesTemplate
- Template:Algorithm-begin
- Template:Algorithm-end
- Template:Cite book
- Template:Cite journal
- Template:Commons category
- Template:Infobox algorithm
- Template:Reflist