Enter DPLL! - An Introduction
Ever wondered how computers solve those tricky SAT problems? Meet the DPLL algorithm, a cornerstone in the world of logic puzzles. What does DPLL stand for? Its very creators Davis, Putnam, Logemann, and Loveland! It's a classic in the field of computer science, simplifying complex problems by systematically exploring possible solutions.
What is DPLL??
DPLL algorithm is designed to determine the satisfiability of logical formulas. It is essentially a "Trial and Error" method, but more sophisticated. The algorithm works by systematically exploring possible assignments and simplifying the formula through techniques like unit propagation and pure literal elimination. This process reduces the complexity of the problem, making it easier to find a solution or prove that no solution exists.
So, how does it work?
- Unit Propagation: Unit literals are assigned TRUE (Because if they are not, the clause and in turn the whole sentence would become FALSE). When a literal (a unit) is assigned, the effects fall upon the clauses containing either the literal or its negated version. There are two points to be noted:
1. clause contains literal
A clause is true if any literal is true, even if the other literals do not yet have truth values
Hence, the clause can be removed from the list of clauses that make the problem (a sentence).
For example, the sentence (A ∨ B ∨ C) is true if A is true, regardless of the values of B and C.
2. clause contains -literal
A sentence is false if any clause is false, which occurs when each of its literals is false. This can occur long before the model is complete.
So, the literals that become FALSE because of the new assignment can be removed from corresponding clauses.
Pure Literal Elimination: Next, it is about literals that only appear in one form (either always positive or always negative) also called "pure literals". These are assigned TRUE (For obvious reasons - A literal that is never negated cannot be the cause of a failure when it is assigned and only aids in satisfying the clause and the sentence).
Splitting: Finally, the remaining subproblems are tackled by choosing a variable and assigning it a value. If the assigned value leads to FAILURE, the alternate value is assigned after backtracking. To improve the algorithm further, a heuristic can be employed to choose the variable.
Success or Failure: This is determined by examining the list of clauses. Because of unit propagation done after each assignment, clauses might get removed or shortened.
No clauses in the list would mean that every clause was deemed TRUE and got removed from the list. So, the assignments done so far are returned, indicating success.
An empty clause in the list suggests that every literal belonging to the clause was deemed FALSE and was removed from the clause. This means that the whole sentence is FALSE and FAILURE (None) is returned.
Pseudocode
Artificial Intelligence - A Modern Approach
(Third Edition) by Stuart J. Russell and Peter Norvig
Implementation in Python
# Functions
find_pure_literals(clauses)
unit_propagation(clauses, unit)
dpll(clauses, assignmemt)
def find_pure_literals(clauses):
''' Returns list of pure literals present in the provided list of clauses
'''
pure_literals = []
for clause in clauses:
for literal in clause:
if literal not in pure_literals:
pure_literals.append(literal) # adds all literals
pure_literals = [x for x in pure_literals if -x not in pure_literals] # retains pure literals and filters out others
return pure_literals
def unit_propagation(clauses, unit):
''' Eliminates the clauses that contain 'unit'
Shortens the clauses that contain '-unit'
Returns the list of clauses after the above modifications
'''
new_clauses = []
for clause in clauses:
if unit in clause:
continue # removing true clauses (clauses with 'unit')
new_clause = [x for x in clause if x != -unit] # shortening clauses with '-unit'
new_clauses.append(new_clause)
return new_clauses
def dpll(clauses, assignment):
'''
Returns the current assignment if no more clauses in the list
None if empty clauses found (FAILED TO SATISFY)
Assign pure literal TRUE, if any
Assign unit literal TRUE, if any
Choose a variable, assign FALSE, proceed for other literals:
If the result is FAILURE, remove the assignment
(BACKTRACK), assign TRUE and return the result (success
or failure, whatever!)
Else return the result
Note: The assigned pure literals, chosen variables are also propagated just like unit literals
'''
if not clauses:
return assignment
if any([len(clause)==0 for clause in clauses]):
return None
for clause in clauses:
if len(clause)==1: # unit literal
unit = clause.pop()
clauses = unit_propagation(clauses, unit)
assignment.append(unit)
return dpll(clauses, assignment)
pure_literals = find_pure_literals(clauses)
if pure_literals:
for unit in pure_literals:
clauses = unit_propagation(clauses, unit)
assignment.append(unit)
return dpll(clauses, assignment)
variable = clauses[0].pop() # chosen var - first literal in the first clause found in the list of clauses
result = dpll(unit_propagation(clauses, -variable), assignment + [-variable]) # modify clauses, assignments and pass as params
if result:
return result
return dpll(unit_propagation(clauses, variable), assignment + [variable])
# main
cnf1 = [{1, -3, 4}, {-1, 2, 3}, {-2, -3, 4}, {1, -2, 3}, {-1, 2, -4}, {1, 2, -3}, {-1, -2, 3}, {1, -3, -4}, {-1, 3, 4}, {2, -3, 4}]
cnf2 = [{1, -2, 3}, {-1, 2, -3}, {1, 2, 3}, {-1, -2, -3}, {1, -3, 4}, {-1, 3, -4}, {2, -3, 4}, {-2, 3, -4}, {1, -2, 4}, {-1, 2, -4}]
cnf3 = [{-1, -2}, {-1, -3}, {-2, -3}, {1, 2}, {1, 3}, {2, 3}]
cnf_list = [cnf1, cnf2, cnf3]
for i,cnf in enumerate(cnf_list):
result = dpll(cnf, [])
if result:
print(f"CNF {i+1} is satisfiable with the following assignment: \n{result}")
else:
print(f"CNF {i+1} is unsatisfiable\n[]")
Advantages (And also Limitations:)
I don't intend to make this post any longer, so here's a brief overview regarding the pros and cons -
- DPLL is highly efficient for many practical SAT problems (mainly due to its use of awesome techniques like unit propagation and pure literal elimination)
- Also, it is complete (it WILL find a solution, if one exists)
This algorithm forms the basis for many modern SAT solvers, which are used in various applications such as automated theorem proving, hardware verification, and artificial intelligence. (I just cited that from Wikipedia, but whatever; I know it's true)
In the worst case, the DPLL algorithm has an exponential time complexity.
It can consume a significant amount of memory, especially for large instances.
The performance can be heavily dependent on the heuristics used for variable selection and decision making. Poor heuristics can lead to inefficient searches and longer solution times.
Applications? (My, My...)
By this time, you already know that this algorithm is designed for solving SAT problems. Therefore, it follows that any problem which can be modeled as SAT problem is indeed solvable using DPLL!
Conclusion
You've been exposed to DPLL Algorithm to solve satisfiability problems. That's what the conclusion is! So, grab a coffee, roll up those sleeves, and go Plus Ultra on DPLL. NOW!
References
- This post is meant to be an (assignment-level) introduction on DPLL. So, if you're really into it (like wanting to explore heuristics for choosing variable), become a search ninja on Google (Sure, you did your research, but hey, there's always more to discover!)
- Also, I'd recommend going through the textbook yourself once.
- I found these slides really helpful and definitely recommend.
Top comments (0)