Current Work
Current work on improving the algorithm has been done on three directions: defining different policies for choosing the branching literals; defining new data structures to make the algorithm faster, especially the part on unit propagation; and defining variants of the basic backtracking algorithm. The latter direction include non-chronological backtracking (aka. backjumping) and clause learning. These refinements describe a method of backtracking after reaching a conflict clause which "learns" the root causes (assignments to variables) of the conflict in order to avoid reaching the same conflict again.
A newer algorithm from 1990 is Stålmarck's method. Also since 1986 (reduced ordered) binary decision diagrams have also been used for SAT solving.
Read more about this topic: DPLL Algorithm
Famous quotes containing the words current and/or work:
“You are the current of the frozen stream,
Shadow invisible, ambushed and vigilant flame.”
—Allen Tate (1899–1979)
“Irish was a man of parts even if some of them didn’t work too well.”
—Angela Carter (1940–1992)