Boolean Satisfiability Problem
The Boolean Satisfiability Problem is one in which we have to decide if there exists an assignment for
some boolean variables that would make a boolean formula evaluate to true.
● If a formula has an assignment under which the formula evaluates to True, then it is
satisfiable.
● If no such assignment exists for a formula, then it is unsatisfiable.
In general, the Boolean Satisfiability Problem can take a very long time to solve (in fact, it’s
NP-Complete).
● If a boolean formula has n variables, then there are 2^n possible assignments. All known
algorithms, in the worst case, will have to do a full search on that exponentially sized search
space.
● However, in real world problems, there are often logical structures in the problem that an
algorithm can utilize to search better.
Two algorithms that try to find a satisfying assignment for a formula (SAT solvers):
● Davis-Putnam-Logemann-Loveland Algorithm, which forms the basis for modern SAT
solving algorithms today.
● Conflict-Driven Clause Learning Algorithm, which improves on the first algorithm.
Both algorithms will only work on boolean formulas that are in Conjunctive Normal Form (CNF).
● In this form:
○ Boolean formulas are composed of the ANDs (∧) of clauses
○ Clauses are the ORs (v) of literals
○ Literals are a variable or its negation
Formulas in CNF have some nice properties that make reasoning quick.
● Since the formula is just the clauses ANDed together, for our formula to be satisfied every
clause must be satisfied.
● Since each clause is made of the ORs of literals, only one literal needs to be satisfied for the
whole clause to be satisfied.
Boolean Constraint Propagation
When an algorithm searches for a satisfying assignment for a CNF formula, one optimization is to look
for unit clauses.
● A clause is unit under a partial assignment when that assignment makes every literal in the
clause unsatisfied but leaves a single literal undecided.
Because the clause must be satisfied for the formula to be satisfied, there’s no point in checking any
assignment that would make that undecided literal false. The algorithm can just make its next guess
such that the literal will be true and thus the clause true.
3
,This process is known as Boolean Constraint Propagation* (BCP). Algorithms will run BCP to
assign variables that logically only have one option due to unit clauses. Sometimes, doing BCP for
unit clauses will cause other clauses to become unit! Algorithms will run BCP repeatedly until there
are no unit clauses.
*BCP equals the simplification steps that follow from a unit literal.
Davis-Putnam-Logemann-Loveland Algorithm
The DPLL algorithm is a SAT solver based on recursive backtracking that makes use of BCP. While a
naive recursive backtracker would check every possible assignment until it found one that satisfies the
formula, DPLL makes BCP-driven inferences to cut down on the size of the search tree – removing
assignments that can’t satisfy the formula. When it encounters a conflict, it backtracks to the last
non-BCP decision it made, and makes the other choice.
Here’s the pseudo-code:
DPLL:
Run BCP on the formula.
If the formula evaluates to True, return True.
If the formula evaluates to False, return False.
If the formula is still Undecided:
Choose the next unassigned variable.
Return (DPLL with that variable True) || (DPLL with that variable False)
See how DPLL works with the example below. On the left, we have a visualization of the decision tree
which shows the history of choices that the algorithm makes. Edges that are solid represent the
guesses/decisions the algorithm makes, while edges that are dashed represent that the algorithm
used BCP to get that choice. The path in blue leads to where the algorithm currently is at.
Conflict Driven Clause Learning
DPLL has three shortcomings.
● It makes naive decisions.
● When it encounters a conflict, it doesn’t learn anything else from the conflict besides the fact
that the current partial assignment led to the conflict.
● It can only backtrack one level which can cause it to keep exploring a search space that is
doomed to fail.
Conflict Driven Clause Learning (CDCL) improves on all three aspects! We’ll focus on the
improvements that CDCL makes on the last two shortcomings:
● clause learning from conflicts
● non-chronological backtracking
Clause Learning
When CDCL reaches a conflict, it looks at the guesses it has made, and all of the assignments it was
forced to infer via BCP which eventually led to the conflict.
4
, ● If we graph out these guesses and their implications, we get a graph called the implication
graph. This is the graph of the decisions it made, the literals that were BCP’d and why, and
how it got to the conflict.
● By looking at this graph, CDCL is able to learn a clause that is potentially more useful than
just the knowledge that the current partial assignment was bad.
● This way, CDCL can avoid making the same mistake over and over and skip over large
chunks of bad partial assignments DPLL will get stuck in.
What’s great about the learned clause is that it allows CDCL to learn from its mistakes and ignore
huge sections of the search space that will never satisfy the formula.
Once CDCL has learned a clause, CDCL will be able to backtrack potentially more than one level, and
BCP using the learned clause to put what it learned into action immediately. The ability to backtrack
more than one level with the learned clause is what we call non-chronological backtracking.
5
The benefits of buying summaries with Stuvia:
Guaranteed quality through customer reviews
Stuvia customers have reviewed more than 700,000 summaries. This how you know that you are buying the best documents.
Quick and easy check-out
You can quickly pay through credit card or Stuvia-credit for the summaries. There is no membership needed.
Focus on what matters
Your fellow students write the study notes themselves, which is why the documents are always reliable and up-to-date. This ensures you quickly get to the core!
Frequently asked questions
What do I get when I buy this document?
You get a PDF, available immediately after your purchase. The purchased document is accessible anytime, anywhere and indefinitely through your profile.
Satisfaction guarantee: how does it work?
Our satisfaction guarantee ensures that you always find a study document that suits you well. You fill out a form, and our customer service team takes care of the rest.
Who am I buying these notes from?
Stuvia is a marketplace, so you are not buying this document from us, but from seller vjblom. Stuvia facilitates payment to the seller.
Will I be stuck with a subscription?
No, you only buy these notes for $6.43. You're not tied to anything after your purchase.