Дэвис-Путнэм-Логеманн-Ловеланд алгоритмі және қанағаттандыру мәселесінің шешімі

Type of search 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. 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.

The SAT problem is important both from theoretical and practical points of view. In complexity theory it was the first problem proved to be NP complete, and can appear in a broad variety of applications such as model checking, automated planning and scheduling, and diagnosis in artificial intelligence. As such, writing efficient SAT solvers has been a research topic for many years. GRASP (1996 1999) was an early implementation using DPLL. and MiniSat were in the first places of the competitions in 2004 and 2005. Another application that often involves DPLL is automated theorem proving or satisfiability modulo theories (SMT), which is a SAT problem in which propositional variables are replaced with formulas of another mathematical theory.

Since 1986, (Reduced ordered) binary decision diagrams have also been used for SAT solving. In 1989 1990, Stålmarck's method for formula verification was presented and patented. It has found some use in industrial applications. DPLL has been extended for automated theorem proving for fragments of first order logic by way of the DPLL(T) algorithm. In the 2010 2019 decade, work on improving the algorithm has found better policies for choosing the branching literals and new data structures to make the algorithm faster, especially the part on unit propagation. However, the main improvement has been a more powerful algorithm, Conflict Driven Clause Learning (CDCL), which is similar to DPLL but after reaching a conflict "learns" the root causes (assignments to variables) of the conflict, and uses this information to perform non chronological backtracking (aka backjumping) in order to avoid reaching the same conflict again. Most state of the art SAT solvers are based on the CDCL framework as of 2019.

Runs of DPLL based algorithms on unsatisfiable instances correspond to tree resolution refutation proofs.