SAT Solvers
Logic in Computer Science
1
SAT Solvers: Decide if a set of clauses is satisfiable.
• Fundamental problem from theoretical point of view – Cook Theorem, 1971: the first NP-complete problem.
• Numerous applications:
– Solving any NP problem…
– Verification: Model Checking, theorem-proving, …
– AI: Planning, automated deduction, …
– Design and analysis: CAD, VLSI
– Physics: statistical mechanics (models for spin-glass material)
• Tools: Semantics Tableau, Resolution, DPLL, …
2
1
Annual Competitions
• SAT Competition
• http://www.satcompetition.org/
• SMT-COMP
• https://smt-comp.github.io/2020/
• Constraint Satisfaction Solver Competition • http://xcsp.org/competition
• QBF Solvers Evaluation
• http://www.qbflib.org/index_eval.php
• Open Source Solvers: SATLIB, minisat, …
3
SAT basic definitions: clauses
• The state of an n-literal clause C under a partial assignment is:
– Satisfied if at least one of C’s literals is satisfied,
– Conflicting if all of C’s literals are unsatisfied,
– Unit if n-1 literals in C are unsatisfied and 1 literal is unassigned, and
– Unresolved if the clause is not satisfied and more than one literal are unassigned.
4
2
Clause states: Examples
5
Basic definitions: the unit clause rule
• The unit clause rule: In a unit clause the unassigned literal must be satisfied.
• Boolean Constraint Propagation (BCP): Repeatedly apply the unit clause rule until no more new unit clauses can be generated or an empty clause is generated.
C {A}
• BCP is a decision procedure for Horn clauses.
A
C
6
3
A Basic SAT algorithm without BCP
Given inCNF:(x|y|z),(-x|y),|(-y|z),(-x|-y|-z)
x -x
y -y z -z ()
z -z X y -y () () ()
Decide()
Deduce()
(y),(-y,z),(-y,-z)
(y,z),(-y,z)
(z),(-z)
()
(y),(-y)
()
X X X X Resolve_Conflict()
7
DPLL Algorithm (recursive) DPLL: Davis-Putnam-Logemann-Loveland
procedure DPLL(S, α): Boolean
// α: list of unit clauses; S: clause set, including α S = BCP(S, α); // apply unit-clause rule
if in S return false // UNSATISFIABLE;
if (S = α) return true // SATISFIABLE; Choose a decision literal p occurring in S – α;
if DPLL(S U {(p)}, α U {p}) return true;
if DPLL(S U {(¬p)}, α U {¬p}) return true; return false // UNSATISFIABLE;
8
4
Basic Backtracking Search
Organize the search in the form of a decision tree
• Each internal node corresponds to a decision
• Depth of the node in the decision tree is called the decision level
• Notation: x=v@d
x is assigned value v in {0,1} at decision level d
9
Backtracking Search in Action
x1 x1 = 0@1
x2 =0@2 x3 =1@2byc1
x2
x1 =1@1x4 =0@1byc2 x2 =0@1byc3
x3=1@1byc1 {x1=1, x2=0, x3=1 , x4=0}
x2 =1@2x4 =1@2byc3 {x1=0, x2=1, x4=1}
{x1=0, x2=0, x3=1}
c1 =(x2|x3)
c2 = (x1 | x4) c3 = (x2 | x4)
10
5
Backtracking Search in Action
c1 =(x2|x3)
c2 = (x1 | x4)
c3 = (x2 | x4)
c4 =(x1|x2|x3)
x1 = 1@1 x4 =0@1byc2 x2 = 0@1 by c3
x3 =1@1byc1 conflict
Add a clause c4 x1
x1 = 0@1 x2
x2 =0@2 x3 =1@2byc1 {x1=0, x2=0, x3=1}
11
Decision Tree of DPLL
c1 =(x2|x3|x5)
c2 = (x1 | x4)
c3 = (x2 | x4)
c4 =(x1|x2|x3) c5 = (x5 )
x5 @0
x1 = 1
conflict
x1 = 0
x1
x2
x2 = 1
{ x1, x2, x4, x5 }
x1 @1
x1 @1 x4 @1 by c2 x2 @1 by c3 x3 @1 by c1 c4 is a conflict
x2 = 0
{ x1, x2, x3, x5 }
x2 @2 x4 @2 by c3
x2 @2
x3 @2 by c1
12
6
Non-Recursive SAT algorithm (DPLL-based)
Implicit Data: S: clauses
α: stack of literal assignments (unit clauses)
level: number of decided literals in α Choose the next variable
while (true) {
and value. Return False if all variables are assigned
}
if (!Resolve_Conflict()) return (UNSAT);
if (!Decide()) return (SAT); while (!Deduce())
Apply BCP. Return False if reached a conflict
Backtrack until no conflict. Return False if impossible
13
Embellishing DPLL
• Branch selection heuristics • Clause Learning
• Backjumping heuristics
• Watched literals
• Randomized restarts
• Symmetry breaking
• More powerful deduction systems •…
14
7
Decide()
• Picks an unassigned variable • Gives it a value
• Push on decision stack
– Efficient structure for depth-first search tree
15
15
Data Structures
• Variable array
• Clause “DB”
• Each clause is a list of literals • Decision “stack”
stack vars clause DB
16
16
8
Tracking Variable Assignments
• Each assignments made at some tree level
– They can be divided into “decision” and “implied”
– Has associated decision stack height
• On backtrack
– Undo assignments
17
17
Decision heuristics for Decide() DLIS (Dynamic Largest Individual Sum)
• Maintain a counter for each literal: in how many unresolved clauses it appears ?
• Decide on the literal with the largest counter.
• Requires O(#literals) queries for each decision.
18
9
Various Branch Selection Heuristics
• Random
• Max occurrence in clauses of min size
• Max occurrence in as yet unsatisfied clauses
• With probability proportional to some function of how often the literal appears in partial assignments that lead to unsatisfiable restricted formulae.
•…
19
}
if (!Resolve_Conflict()) return (UNSAT);
Non-Recursive SAT algorithm (DPLL-based)
Implicit Data: S: clauses
α: stack of literal assignments
level: number of decided literals in α
while (true) {
Choose the next variable and value. Return False if all variables are assigned
if (!Decide()) return (SAT); while (!Deduce())
Apply BCP, Return False if reached a conflict
Backtrack until no conflict. Return False if impossible
20
10
Deduce()
• Tradeoff between searching more partial assignments (going deeper in the tree), and searching for proofs of unsatisfiability higher up in the tree.
• Currently, deduction is typically just BCP, i.e., iterated unit-propagation.
• (OtherembellishmentstoDPLLseemtorender more complex deduction unhelpful in practice.)
21
Naive Implementation of Deduce
• Check every clause after an assignment is made and reduce it if possible
–Repeat if a unit clause is generated (implication)
• After backtrack, revert all clauses to their original form as they were before.
• A solver would spend 85-90% of the time doing unit propagation
• Why not use the idea of head/tail literals?
22
11
Deduce()
• What do we need to do on each variable assignment?
– Find unit clauses
• When all literals in a clause are false except one • Look through all clauses this assignment effects • See if any now have all false and one unassigned
– Assign implied values by unit clauses – Propagate that assignment
– Conflict if the unit clause is false
23
23
• Q := new queue(); // of literals Deduce() • Q.insert(top of decision stack);
while (!Q.empty())
x := Q.pop();
for each clause C in DB which contains x
if C has one unassigned literal, rest are false y := unassigned literal in C
If value(y) = 0 return (false); // conflict If value(y) = 1 continue; // already true value(var(y)) := sign(y); // assign 0 or 1 Q.add(y);
return(true)
24
24
12
Avoiding Clause Visits
• Idea: watch only 2 literals in each clause: head/tail
literals
• Only care about the last two literals of the clauses which are assigned a value.
• If other k-2 are assigned, won’t force a unit clause
• Get a unit clause when one of the last two literals (and everything else are assigned false)
• Relax the positions of the head/tail literals: They don’t have to be the first/last unassigned literals.
• They are called “watched literals”
• Advantage: No undo-work when backtracking 25
25
Data Structure for Clauses
Counter Implementation
Watch Literal implementation 26
26
13
BCP Algorithm: Example
Watched literals are underlined.
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1 | v4)
(-v1)
• Initially, we identify any two literals in each clause as the watched ones (they could be first/last literals) • Clauses of size one are a special case
27
BCP Algorithm: Example
We begin by processing the assignment v1 = 0, which is implied by the unit clause (-v1)
Stack: (v1=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1 | v4)
28
14
BCP Algorithm: Example
Stack:(v1=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
We must examine each clause where the assignment being processed has set a watched literal to 0.
29
BCP Algorithm: Example
Stack:(v1=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1 | v4)
• We must examine each clause where the assignment being processed has set a watched literal to 0
• We need not process clauses where a watched literal has been set to 1, because the clause is now satisfied and so can not become unit.
30
15
BCP Algorithm: Example
Stack:(v1=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1 | v4)
• We must examine each clause where the assignment being processed has set a watched literal to 0
• We need not process clauses where a watched literal has been set to 1, because the clause is now satisfied and so can not become unit.
• We certainly need not process any clauses where neither watch literal changes state (in this example, where v1 is not watched).
31
BCP Algorithm: Example
• Now let’s actually process the second and third clauses:
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1 | v4) Stack:(v1=0)
• For the second clause, we replace v1 with -v3 as a new watched literal.
• Since -v3 is not assigned to 0, it can be a good watch literal.
32
16
BCP Algorithm: Example
(v2 | v3 | v1 | v4 | v5)
(v1 | v2 | -v3)
(v1 | -v2) (v1 | -v2)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(-v1| v4) Stack:(v1=0)
(-v1| v4) Stack:(v1=0) Pending: (v2=0)
•The third clause is unit. We record the new unit (-v2) in the pending queue of assignments to process.
33
BCP Algorithm: Example
• Next, we process (-v2); only examine the first 2 clauses
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0, v2=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0, v2=0) Pending: (v3=0)
In the first clause, we replace v2 with v4 as a new watched literal, since v4 is not assigned to 0.
The second clause is unit, and we add (-v3) to the queue of assignments to process.
34
17
BCP Algorithm: Example
• Next, we process (-v3). We only examine the first clause.
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0, v2=0, v3=0)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0, v2=0, v3=0) Pending:
For the first clause, we replace v3 with v5 as a new watched literal.
Since no pending assignments, and no conflict, BCP stops. We make a decision. Both v4 and v5 are unassigned. Let’s say we decide to assign v4=0 and proceed.
35
BCP Algorithm: Example
• Next, we process (-v4). We need to check the first and last clauses.
(v2 | v3 | v1 | v4 | v5)
(v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4) (-v1| v4)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
Stack:(v1=0, v2=0, v3=0, v4=0)
Stack:(v1=0, v2=0, v3=0 , v4=0) Pending: (v5=1)
First clause becomes unit. We add (v5) into the pending queue.
Last clause is satisfied because of -v1; we do nothing.
36
18
BCP Algorithm: Example
• Next, we process (v5). No clauses to be checked.
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0, v2=0, v3=0, v4=0, v5=1)
(v2 | v3 | v1 | v4 | v5) (v1 | v2 | -v3)
(v1 | -v2)
(-v1| v4)
Stack:(v1=0, v2=0, v3=0 , v4=0, v5=1)
Pending:
Since there are no pending assignments, and no conflict, BCP stops.
No variables are unassigned, so the instance is SAT, and we are done with a model in the stack.
37
Practice Questions
Given the following clauses, assuming the first two literals of each clause are their initial watch literals, what are the states of these clauses after BCP with the partial interpretation α ={x1=0, x2=0}? And what are the watch literals in these clauses?
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
38
19
Practice Questions
Given the following clauses, assuming the first two literals of each clause are their initial watch literals, what are the states of these clauses after BCP with the partial interpretation α ={x1=0, x2=0}? And what are the watch literals in these clauses?
First two literals are watched. After processing (-x1), (-x2). Pending: (-x3)
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
39
Practice Questions
Given the following clauses, assuming the first two literals of each clause are their initial watch literals, what are the states of these clauses after BCP with the partial interpretation α ={x1=0, x2=0}? And what are the watch literals in these clauses?
Process (-x3) After processing (-x3). Pending: (x4),
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
40
20
Practice Questions
Given the following clauses, assuming the first two literals of each clause are their initial watch literals, what are the states of these clauses after BCP with the partial interpretation α ={x1=0, x2=0}? And what are the watch literals in these clauses?
Process (x4) After processing (x4). Pending:
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
c1 =(x1|x2|x3|x4|x5) c2 =(x1|x2|x4 ) c3 =(x2|x3|x4 )
c4 =(x1|x2|x3 )
41
Example: Graph Coloring
Given an undirected graph G = (V, E), the graph coloring problem is to assign each vertex a color such that no two adjacent vertices receive the same color. Specify a propositional formula A such that G can be colored using at most C colors iff the formula A is satisfiable.
Every vertex must have a unique color.
(pa,1 | pa,2), (pb,1 | pb,2), (pc,1 | pc,2), (pb,1 | pd,2), (pe,1 | pe,2),
(¬pa,1 | ¬pa,2), (¬pb,1 | ¬pb,2), (¬pc,1 |
¬pc,2), (¬pd,1 | ¬pd,2), (¬pe,1 | ¬pe,2). Adjacent vertices have different colors (¬pa,1 | ¬pb,1), (¬pa,2 | ¬pb,2),
(¬pa,1 | ¬pd,1), (¬pa,2 | ¬pd,2),
(¬pa,1 | ¬pe,1), (¬pa,2 | ¬pe,2), (¬pb,1 | ¬pc,1), (¬pb,2 | ¬pc,2), (¬pc,1 | ¬pd,1), (¬pc,2 | ¬pd,2).
42
21
Example: Graph Coloring
Every vertex must have a unique color.
(pa,1 | pa,2), (pb,1 | pb,2), (pc,1 | pc,2), (pb,1 | pd,2), (pe,1 | pe,2),
(¬pa,1 | ¬pa,2), (¬pb,1 | ¬pb,2), (¬pc,1 | ¬pc,2), (¬pd,1 | ¬pd,2), (¬pe,1 | ¬pe,2).
Adjacent vertices have different colors (¬pa,1 | ¬pb,1), (¬pa,2 | ¬pb,2),
(¬pa,1 | ¬pd,1), (¬pa,2 | ¬pd,2),
(¬pa,1 | ¬pe,1), (¬pa,2 | ¬pe,2),
(¬pb,1 | ¬pc,1), (¬pb,2 | ¬pc,2), (¬pc,1 | ¬pd,1), (¬pc,2 | ¬pd,2).
An instance of 2CNF.
Now run DPLL on it.
Choose pa,1 = 1
pa,2 = 0 by (¬pa,1 | ¬pa,2) pb,1 = 0 by (¬pa,1 | ¬pb,1) pb,2 = 1 by (pb,1 | pb,2) pc,2 = 0 by (¬pb,2 | ¬pc,2) pc,1 = 1 by (pc,1 | pc,2) pd,1 = 0 by (¬pc,1 | ¬pd,1) pd,2 = 1 by (pd,1 | pd,2) pe,1 = 0 by (¬pa,1 | ¬pe,1) pe,2 = 1 by (pe,1 | pe,2)
A model is found.
Now let pa,1 = 0
…
43
}
if (!Resolve_Conflict()) return (UNSAT);
Non-Recursive SAT algorithm (DPLL-based)
Implicit Data: S: clauses
α: stack of literal assignments
level: number of decided literals in α
while (true) {
Choose the next variable and value. Return False if all variables are assigned
if (!Decide()) return (SAT); while (!Deduce())
Apply BCP, Return False if reached a conflict
Backtrack until no conflict. Return False if impossible
44
22
Resolve_Conflict()
• What does Resolve_Conflict need to do?
– Look at most recent decision (e.g. x = 0)
– If can go other way (e.g., x = 1), switch value
• (undo assignments to this depth)
– Else pop and recurse on the previous decision – If no more decisions to pop,
• unsatisfiable
45
45
DPLL Algorithm with Levels
Implicit Data: S: clauses
α: stack of literal assignments
level: number of decided literals in α
while (true) {
if (Decide()) { //1. Branching – increase level
while (!Deduce()) { //2. Deducing
backlevel = analyze_conflicts() // 3. Learning if (backlevel < 0)
return False // or UNSAT else backtrack(blevel)
// 4. Backtracking – reduce level
}
else return True // i.e., SAT
}
Detail of Resolve_conflict()
46
23
Learning
• Adding information about the input instance into the solution process without changing the satisfiability of the problem.
– In CNF representation, it is accomplished by adding clauses into the clause database
• Knowledge of failure may help search in other portions of the search space.
• Learning is very effective in pruning the search space for structured problems
– It is of limited use for random instances – Why? Still an open question
47
Clause Learning
• When DPLL discovers (S, α) is unsatisfiable, it derives (learns) a reason for this in the form of new clauses to add to the input clauses.
• What clauses are learned, and how, make huge differences in performance.
• Trivially learned clause: if (S, α) is unsatisfiable for
α = {x1, x2, ..., xk }, derive clause {¬x1, ¬x2, ..., ¬xk}
But we want short clauses that constrain the solution space as much as possible...
48
24
A Small Example
– Variables numbered x1 to x9
– Formula consists of clauses c1 to c6 :
c1 =(x1 |x2)
c2 =(x1 |x3 |x7 )
c3 =(x2 |x3 |x4 ) c4 =(x4 |x5 |x8 ) c5 =(x4 |x6 |x9 ) c6 =(x5 |x6 )
Start by choosing literal x7 with assignment x7 = 0 (decision level 1)
49
Motivation
assume BCP returns new unit clauses
c1 =(x1 |x2)
c2 =(x1|x3 |x7 )
c3 =(x2 |x3 |x4 ) c4 =(x4 |x5 |x8 ) c5 =(x4 |x6 |x9 ) c6 =(x5 |x6 )
x7=0@1 BCP=Ø x8=0@2 BCP=Ø
x9=0@3 BCP=Ø
x1 = 0@4 BCP = {x2=1, x3=1, x4=1, x5=1, x6=1}
c6 is conflicting
BCP adds nothing at decision levels 1, 2 and 3. BCP at level 4 leads to a conflicting clause c6.
50
25
c1 =(x1 |x2)
c2 =(x1|x3 |x7)
c3 =(x2 |x3 |x4) c4 =(x4 |x5 |x8) c5 =(x4 |x6 |x9) c6 =(x5 |x6)
x7=0@1 BCP=Ø x8=0@2 BCP=Ø
x9=0@3 BCP=Ø
x1 = 0@4 BCP = {x2=1, x3=1, x4=1, x5=1, x6=1}
Generation of New Clause
c6 is conflicting
new := c6 = (x5 | x6 ) // the conflicting clause.
Latest assignment: x6=1 by c5 = (x4 | x6 | x9)
Resolution of new and c5 : new := (x4 | x5 | x9)
Latest assignment: x5=1 by c4 = (x4 | x5 | x8)
Resolution of new and c4 : new := (x4 | x8 | x9), which is kept.
51
c1 =(x1 |x2)
c2 =(x1|x3 |x7)
c3 =(x2 |x3 |x4) c4 =(x4 |x5 |x8) c5 =(x4 |x6 |x9) c6 =(x5 |x6)
c7 =(x4 |x8|x9)
x7=0@1 BCP=Ø x8=0@2 BCP=Ø
x9=0@3 BCP=Ø
x1 = 0@4 BCP = {x2=1, x3=1, x4=1, x5=1, x6=1} c6 is conflicting
Effect on Backtracking
Backtrack to level = max{ level(x) | x is an element of new, x L, L is the literal of maximal level in new}.
e.g.,L=x4 level=3
52
26
Effect on Backtracking
No need to consider the second branch of x1 and we backjump to level 3.
c1 =(x1 |x2)
c2 =(x1|x3 |x7)
c3 =(x2 |x3 |x4) c4 =(x4 |x5 |x8) c5 =(x4 |x6 |x9) c6 =(x5 |x6)
c7 =(x4 |x8|x9)
We reconsider x1 = 0.
x7=0@1 BCP=Ø x8=0@2 BCP=Ø
x9=0@3 BCP={x4=0byc7}
x1 =0@4 BCP={x2=1byc1,x3=1byc2 }
c3 is conflicting
new:=Resolve(c3,c2 )=(x1|x2 |x4 |x7) new:=Resolve(new,c1 )=(x1 |x4 |x7)
53
Conflict-driven Clause Learning
• Use the conflict clause to guide the search. • Details of analyze_conflicts():
1. 2. 3. 4. 5. 6. 7. 8.
Lvl := the current level.
newClause = conflict_clause
while newClause has more than one literal assigned at Lvl
Pick the literal L, last assigned in newClause
Resolve L off between newClause and the clause forced L. Let newClause be the resolvent of the above resolution.
Add newClause into S
return the second highest level in newClause
54
27
Generate New Clause from Conflict Clause
x1 x1 = 1@1
x4 =0@1byc2 x2 =0@1byc3
x3 =1@1byc1
c4 conflict
c nc0 = c4
1 Please generate a new clause c3
from the conflict by the
Algorithm in the previous side. c2
nc1 =(x1 |x2 ) nc2 =(x1 |x4 ) nc3 =(x1 )
c1 =(x2|x3)
c2 = (x1 | x4)
c3 = (x2 | x4)
c4 =(x1|x2|x3)
55
Generate New Clause from Conflict Clause
c1 =(x1 |x2)
c2 =(x1|x3 |x7 )
c3 =(x2 |x3 |x4 )
c4 =(x4 |x5 |x6 )
c5 =(x3 |x4 )
c6 =(x5 |x6 )
x7=0@1 BCP=Ø
x =0@2 6
BCP=Ø
BCPaddsnothing atdecisionlevels1 and2.Addx at level3. 4
c =(x |x )
BCP={x =0byc }
c7 =(x2 |x3 )
x =0@3 544
x1 = 0@4
BCP = {x2=1 by c1, x3=0 by c3}
c7 is conflicting
BCP at level 4 leads to a conflict clause c7.
c8 =(x1 |x3 |x ) 9123
56
28
Generate New Clause from Conflict Clause
c1 =(x1 |x2)
c2 =(x1|x3 |x7 )
c3 =(x2 |x3 |x4 )
c4 =(x4 |x5 |x6 )
c5 =(x3 |x4 )
c6 =(x5 |x6 )
c7 =(x2 |x3 )
c8 =(x1 |x3 )
c9 =(x1 |x2 |x3 ) x1 =0@4
x7=0@1 BCP=Ø x6=0@2 BCP=Ø
x5=0@3
BCP={x4=0byc4}
BCP = {x2=1 by c1, x3=0byc3}
Newclause: nc0 =c7
nc1 =(x2 |x4 )
c c7 is conflicting 3
57
Generate New Clause from Conflict Clause
c1 =(x1 |x2)
c2 =(x1|x3 |x7 ) c3 =(x2 |x3 |x4 ) c4 =(x4 |x5 |x6 ) c5 =(x3 |x4 )
c6 =(x5 |x6 )
c7 =(x2 |x3 )
c8 = (x1 | x3 )
c9 = (x1 | x2 |x3 ) c10 =(x2 |x4 )
x7=0@1 BCP=Ø x6=0@2 BCP=Ø
x5=0@3 BCP={x4=0byc4} BCP={x =0byc
2 10, x1=1 by c1,
New clause: nc0 = c9
nc1 =(x1 |x2 ) nc2 =(x2 )
x3=1byc8} c9 is conflicting
c8 c1
58
29
Generate New Clause from Conflict Clause
c1 =(x1 |x2)
c2 =(x1|x3 |x7 ) c3 =(x2 |x3 |x4 ) c4 =(x4 |x5 |x6 ) c5 = (x3 | x4 )
c6 =(x5 |x6 )
c7 =(x2 |x3 )
c8 =(x1 |x3 )
c9 =(x1 |x2 |x3 ) c10 =(x2 |x4 )
c11 =(x2 )
Atlevel0: BCP={x2=1byc11,
x3=1byc7,
x4=1byc10 }, c5 is conflicting
11
nc3 = ( )
New clause: nc0 = c5
nc1 =(x2 |x3 ) c nc2 =(x2 )
c10 c7
59
c1 =(x1 |x2)
c2 =(x1|x3 |x7 )
c3 =(x2 |x3 |x4 ) c4 =(x4 |x5 |x8 ) c5 =(x4 |x6 |x9 ) c6 =(x5 |x6 )
c7 =(x3 |x5 )
BCP = {x2=1 by c1, x3=1 by c2, x4=1 by c3,
x5=0 by c7 }
c4 is conflicting
x7=0@1 BCP=Ø
Practice Question:
How to Generate New Clause
x9=0@3 x1 = 0@4
BCP=Ø
x =0@2 8
BCP=Ø
BCPaddsnothing atdecisionlevels 1,2and3.
BCPatlevel4 leads to a conflict clause c4.
60
30
Generate New Clause from Conflict Clause
c1 =(x1 |x2)
c2 =(x1|x3 |x7 )
c3 =(x2 |x3 |x4 )
c4 =(x4 |x5 |x8 )
c5 =(x4 |x6 |x9 )
c6 =(x5 |x6 )
c7 =(x3 |x5 )
x7=0@1 BCP=Ø x8=0@2 BCP=Ø
x9=0@3 BCP=Ø c7
Newclause: nc0 =c4
nc =(x |x |x ) x1=0@4 c1348
BCP = {x2=1 by c1, 3 nc2 =(x2 |x3 |x8 ) x3=1 by c2, c2
x4=1 by c3, c1 nc3 =(x1 |x2 |x7 |x8 ) x5=0 by c7 }
c4 is conflicting nc4 =(x1 |x7 |x8 )
61
Example: n-queen problem
62
31
Boolean Encoding for 4-Queen
• 16Booleanvariablespij,i=1to4,j=1to4
• Constraints are of the form:
• Row and columns queen on location (i,j).”
• (-pij | -pik) for all k = 1 to 4, kj (logical constraint)
• (-pij|-pkj )forallk=1to4,ki • Diagonals
• (-pij |-pi+l,j+l ) for k=1to3,i+k4;j+k4(rightup)
• (-pij |pi-l,j+l ) fork=1to3,i-k1; j+k4(rightdown) • (-pij|-pi-l,j-l ) fork=1to3,i-k1; j-k1(leftdown)
• (-pij |-pi+l,j-l ) for k=1to3,i+k4;j-k1(leftup)
• Need N (= 4) queens on board!
• Foreachrowi: (pi1 |pi2 |pi3 |pi4)
pij = 1 iff “there is a
63
p cnf 16 80
1 2 3 4 0
5 6 7 8 0
9 10 11 12 0 13 14 15 16 0 -12 -16 0
-8 -16 0 -1 -13 0 -1 -6 0 -2 -5 0 ... ...
DIMACS Format for 4-Queen
% p=propositional, cnf=CNF, 16 var., 80 clauses. % 1 = p11, 2 = p12, 3 = p13, 4 = p14
% 5 = p21, 6 = p22, 7 = p23, 8 = p24
% 9 = p31, 10= p32, 11= p33, 12= p34
% 13= p41, 14= p42, 15= p43, 16= p44 %(-p34|-p44)
%(-p24|-p44)
%(-p11|-p41)
%(-p11|-p22) %(-p12|-p21)
64
32
c p=propositional, cnf=CNF, 16 var., 80 clauses. c 1=p11, 2=p12, 3=p13, 4=p14
c 5=p21, 6=p22, 7=p23, 8=p24
c 9=p31,10=p32, 11=p33,12=p34 c13=p41,14=p42, 15=p43,16=p44
-1 -6 0 -1 -11 0 -1-160 -6 -11 0 -6 -16 0 -11 -16 0 -2-70 -2 -12 0 -7-120 -3 -8 0 -5 -10 0 -5-150 -10 -15 0 -9 -14 0 -4-70 -4-100 -4-130 -7 -10 0 -7-130 -10 -13 0 -3 -6 0 -3-90 -6-90 -2 -5 0 -8-110 -8-140 -11 -14 0 -12 -15 0
p cnf 16 80 1234 0 -1-20 -1-30 -1-40 -2-30 -2-40 -3-40 5678 0 -5-60 -5-70 -5-80 -6-70 -6-80 -7-80
9101112 0 -9-100 -9-110 -9-120
15913 0
-1-50 -1-90 -1-130 -5-90 -5-130 -9-130
371115 0 -3-70 -3-110 -3-150 -7-110 -7-150 -11 -15 0 481216 0 -4-80 -4-120 -4-160 -8-120 -8-160 -12 -16 0
-10 -11 0
-10 -12 0
-11 -12 0
13141516 0 261014 0 -13 -14 0
-13 -15 0 -13 -16 0 -14 -15 0 -14 -16 0 -15 -16 0
-2-60 -2-100 -2-140 -6-100 -6-140 -10 -14 0
65
DIMACS Example
Six people sit on a bench of six seats for a group photo: two Americans (A), two Britons (B), a Canadian (C), and a Dane (D). They asked that (i) the distances from the seats taken by the Britons to the middle point of the bench are the same; (ii) either the Canadian or the Americans do not want to sit next to an American; (iii) the Dane likes to sit next to the Canadian. The photographer happily complied. Suppose we use propositional variables Xy, where X ∈ {A, B, C, D} and 1 ≤ y ≤ 6, with the meaning that “Xy is true iff the people of nationality X sits at seat y of the bench”.
• Specify the problem formally in CNF using Xy, such that the models of the CNF matches exactly all the solutions of the photographer.
66
33
c A1=1 A2=2 A3=3 A4=4 A5=5 A6=6 c B1=7 B2=8 B3=9 B4=10 B5=11 B6=12 c C1=13 C2=14 C3=15 C4=16 C5=17 C6=18 c D1=19 D2=20 D3=21 D4=22 D5=23 D6=24
-2 -20 0 -8 -14 0 -8 -20 0 -14 -20 0 -3 -9 0 -3 -15 0 -3 -21 0 -9 -15 0 -9 -21 0 -15 -21 0 -4 -10 0 -4 -16 0 -4 -22 0 -10 -16 0 -10 -22 0 -16 -22 0 ...
p cnf 24 145
c (1) Every seat has c one person:
1 7 13 190
2 8 14 200
3 9 15 210
410 16 220
511 17 230
612 18 240
c (2) Every seat can c sit at most
c one person:
-1 -7 0
-1 -13 0 -1-190 -7 -13 0 -7 -19 0 -13 -19 0 -2 -8 0 -2 -14 0
67
c A1=1 A2=2 A3=3 A4=4 A5=5 A6=6 c B1=7 B2=8 B3=9 B4=10 B5=11 B6=12 c C1=13 C2=14 C3=15 C4=16 C5=17 C6=18 c D1=19 D2=20 D3=21 D4=22 D5=23 D6=24
(5) At most one Canadian: -13 -14 0
-13 -15 0
-13 -16 0
-13 -17 0
-13 -18 0
-14 -15 0
-14 -16 0
-14 -17 0
-14 -18 0
-15 -16 0
-15 -17 0
-15 -18 0
-16 -17 0
-16 -18 0
-17 -18 0
(3) At most two Americans:
-1 -2-30 -1 -2-40 -1 -2-50 -1 -2-60 -1 -3-40 -1 -3-50 -1 -3-60 ...
(4) At most two Britons:
-7 -8 -9 0 -7-8-100 -7-8-110 -7-8-120 -7-9-100 -7-9-110 -7-9-120 -7-10-110 -7-10-120
...
68
34
c A1=1 A2=2 A3=3 A4=4 A5=5 A6=6 c B1=7 B2=8 B3=9 B4=10 B5=11 B6=12 c C1=13 C2=14 C3=15 C4=16 C5=17 C6=18 c D1=19 D2=20 D3=21 D4=22 D5=23 D6=24
(8) American’s neighbor is neither American nor Canadian:
-1 -2 0 -2 -3 0 -3 -4 0 -4-50 -5-60 -1-140 -2-150 -3-160 -4 -17 0 -5 -18 0 -13 -2 0 -14 -3 0 -15 -4 0 -16-50
(6) At most one Dane:
(7) Britons’ seats are symmetric
to the middle: -7120
-1270 -8110 -1180 -9 10 0 -10 9 0
-19 -20 -19 -21 -19 -22 -19 -23 -19 -24 0 -20 -21 0 -20 -22 0 ...
0 0 0 0
69
-17 -6 0
c A1=1 A2=2 A3=3 A4=4 A5=5 A6=6 c B1=7 B2=8 B3=9 B4=10 B5=11 B6=12 c C1=13 C2=14 C3=15 C4=16 C5=17 C6=18
c D1=19 D2=20 D3=21
(9) The Dane likes to sit next to
the Canadian:
-13 20 0
-14 19 21 0 -15 20 22 0 -16 21 23 0 -17 22 24 0 -18 23 0
D4=22 D5=23 D6=24
0
15 0 16 0 17 0 18 0 0
-19 14 -20 13 -21 14 -22 15 -23 16 -24 17
Put every clause in one file, say seats.cnf.
On Linux machine, run
$ minisat seats.cnf result
The file result has a model.
Model#1:1 6 8 11 16 21 Model#2:1 6 8 11 15 22
70
35