---
tag: K7R9D390SP
kind: concept
name: DPLL algorithm
aliases: [davis-logemann-loveland-algorithm, davis-putnam-logeman-loveland-algorithm, davis-putnam-logemann-loveland, davis-putnam-logemann-loveland-algorithm]
sources:
  - wikipedia: en:2745094@r1341870655
    locator: DPLL algorithm
    note: adopted
    mention: wikipedia://en/2745094
    sections: [Summary]
same_as:
  wikidata: Q2030088
  wikipedia: DPLL algorithm
inventory: [217JWT2N1D]
---

## Summary

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|09K9MWD2QQ]] in [[conjunctive normal form|07C4A8Y18K]], i.e. for solving the CNF-SAT problem.