MaxSAT: Maximum Satisfiability
Logic in Computer Science
1
3SAT vs 2SAT
• SAT: Decide if a set of clauses is satisfiable. • 3SAT: Decide if a 3CNF is satisfiable.
• 2CNF: Each clause contains at most 2 literals. • 2SAT: Decide if a 2CNF is satisfiable.
Theorem: 2SAT can be solved in polynomial time.
2
1
2SAT is in P
Theorem: 2SAT is polynomial-time decidable.
Proof: We’ll show how to solve this problem efficiently using path searches in graphs…
3
3
Searching in Graphs
Theorem: Given a graph G=(V,E) and two vertices s,tV, finding if there is a path from s to t in G takes O(|V|+|E|) time.
Proof: Use some search algorithm (DFS/BFS).
4
4
2
Graph Construction
G = (V, E)
• V: Vertex for each variable and the negation of a variable
• E: Edge (, ) iff there exists a clause equivalent to ( | ).
• Every clause (A | B) of 2CNF contributes two edges: (A, B) and (B, A).
5
5
Observation
Claim: If the graph contains a path from to , denoted by , it also contains a path from to .
Proof: If there’s an edge (, ), then there’s also an edge (,). Both edges come from clause ( | ) and .
6
6
3
Correctness
Thereom: A 2CNF formula is unsatisfiable iff there exists a variable x, such that:
1. there is a path from x to x in the graph
2. there is a path from x to x in the graph
That is, x and x are in a cycle.
7
7
Correctness (1)
• Suppose there are paths x x and x x for some variable x, then both x x and x x are true, because the implication relation is transitive. However,
• (x x) (x x) (x x) false
8
8
4
Correctness (2)
•S={(-x|y),(x|-z),(y|z), (-y|z) }
• Suppose v and v are not in a cycle for any v. • Construct an assignment as follows:
1. If there is a path x x,
assign x = 1; If there is a path x x, assign x = 0;
x
yy
2. If there is a path x y, x = 1, assign y = 1.
y
3. Assign arbitrary values to unassigned vertices
9
x x
z
zz
9
Correctness (2)
Claim: The algorithm of assigning truth values is well defined.
Proof: The path relation x y represents the implication x y. If x = 1, then it must be the case that y = 1, so that x y is true.
If there exists a path x x y y, such that x = 1 and y = 0 by the first line of the algorithm, but x y is a violation of the second line, then from x y, we have y x, thus, x, x, y, y are in a cycle, a contradiction to the condition that x, x, are not in a cycle.
10
10
5
2SAT is in P
We get the following efficient algorithm for 2SAT:
–For each variable x find if there is a path from x to x and vice-versa.
–Reject if any of these tests succeeded.
–Accept otherwise. 2SATP.
11
11
2SAT can done in linear time
• Use SCC (Strongly Connected Components) to group vertices which share a common cycle.
• x and x are in a cycle iff they are in the same SCC.
• SCC can be found in the time O(|V|+|E|)
• https://en.wikipedia.org/wiki/Strongly_conne cted_component
12
12
6
2SAT is linear solvable
C={c1:(p|q), c2:(-p|-r),c3:(p|-r), c4:(-q|r),c5:(q|s), c6:(-r|-s)}
Implication graph of C:
q -p -s r
-r s p -q
SSC: Strongly Connected Components
13
2SAT is linear solvable
C={c1:(p|q), c2:(-p|-r),c3:(p|-r), c4:(-q|r),c5:(q|s), c6:(-r|-s)}
S1
S2
q -p -s r
-r s p -q
SCC: S1 = { q, r, -s, -p }, S2 = { p, -q, -r, s }
G’ = ( { S1, S2}, { (S1, S2) }
G’ has no cycles; the topological order is S1, S2. Assign 0 to S1, 1 to S2.
14
7
What is MaxSAT?
The problem of determining the maximum number of clauses, of a given propositional formula in conjunctive normal form (CNF), that can be made true by an interpretation of the formula.
What is the MaxSAT solution for S? S={(p),(p|q),(p|q),(p|r), (p|r),(q|r)} Solutions: = { p, q, r }, { p, q, r }, or { p, q, r }. Five satisfied and one falsified.
15
Why Bother?
• Simply determining that an instance is UNSAT may not be enough.
• We want the optimal way to make the instance satisfiable by allowing for some clauses to be unsatisfied.
• AI
– University course scheduling –…
• EDA (Electronic Design Automation) – Over constrained system analysis
– FPGA routing
–…
16
8
SAT: Propositional Satisfiability
MSAT: Decide if a formula (CNF) is satisfiable 1
17
𝑎∧ (C1) (¬𝑎∨𝑏) ∧ (C2) (¬𝑏∨𝑐) ∧ (C3) 2(¬𝑐∨𝑑)∧ (C4) 3 ¬𝑑 (C5)
17
1
3
Maximum Satisfiability (Max-SAT)
MaxSAT: Find an interpretation to maximize the number of satisfiable clauses, or to
𝑎∧ (C1) (¬𝑎∨𝑏) ∧ (C2) (¬𝑏∨𝑐) ∧ (C3) 2 (¬𝑐∨𝑑) ∧ (C4) ¬𝑑 (C5)
minimize the number of falsified clauses.
Solution: a=1,b=1,c=1,d=1 C5isfalse
18
18
9
Weighted MaxSAT
Weighted MaxSAT: Assign weights to clauses and find an interpretation to maximize an objective.
20: 𝑎∧(C1) 30: ¬𝑎∨𝑏 ∧ (C2) 4:¬𝑏∨𝑐∧ (C3) 22: ¬𝑐∨𝑑∧(C4) 7: ¬𝑑 (C5)
1= 3
Solution: a=1,b=1,c=1,d=0
C4 is false and Objective = 61 (or cost = 2).
19
Maximize
20×C1+30×C2+ 4×C3+2×C4+7×C5 for those satisfied clauses.
Or minimize the cost for those falsified clauses.
19
Hybrid MaxSAT
Hybrid MaxSAT: Clauses are divided into hard/soft subsets; assign weights to soft clauses and find an interpretation to maximize an objective and satisfy all hard clauses.
𝑎∧ (C1) ¬𝑎∨𝑏 ∧ (C2) 1 4: ¬𝑏∨𝑐∧ (C3) 22: ¬𝑐∨𝑑 ∧ (C4)
37: ¬𝑑
(C5)
=
Solution: a=1,b=1,c=1,d=0 C4 is false and Objective = 11 (cost = 2)
Subject to
Maximize or Minimize
C1 and C2ject to
4×C3+2×C4+7×C5 4×C3+2×C4+7×C5
20
20
10
Maximum Clique of a Graph
• Encode the maximum clique problem in MaxSAT • Propositional variables (True means in the clique):
{ a, b, c, d, e }
Hybrid MaxSAT:
Hard = { (-a| -e), (-b | -c), (-c | -e) }
Soft = { (a; 1), (b; 1), (c; 1), (d; 1), (e; 1)}
Weighted MaxSAT:
C = { (-a| -e; 5), (-b | -c; 5), (-c | -e; 5), (a; 1), (b; 1), (c; 1), (d; 1), (e; 1)}
21
Weighted vs Hybrid: Same Power
Increased Expressive Power for Applications
Hard
+
Soft
Soundness Conditions Objectives
Balancing
tradeoffs
(e.g., precision
vs. scalability) specs)
Modeling missing data (e.g., partial programs)
Handling uncertainty (e.g., incorrect
…
22
22
11
Applications of MaxSAT
Many real-world applications can be easily and neatly encoded to MaxSAT:
• Eclipse platform uses MaxSAT for managing the
plugins dependencies
• Error localization in C code
• Debugging of hardware designs
• Reasoning over Biological Networks (Genes)
• Course timetabling
• Final exam scheduling
• …
23
Applications of MaxSAT in Automotive (Re)Configuration
Applications of MaxSAT in Automotive Configuration, by: Rouven Walter and Christoph Zengler and Wolfgang Kuchlin
The after-sales business asks for extensions, replacements, or removal of components of a valid configuration with minimal effort.
Automotive configuration can be represented as a CNF formula in propositional logic, where each model is called a valid configuration of a car. http://ceur-ws.org/Vol-1128/paper3.pdf
24
12
MaxSAT
• Very hard problems — NP-HARD
• Optimization of SAT
• Difficult to find an approximate solution of
the problem
• Large-size MAX-SAT instances cannot be
solved exactly, and one must resort to approximation algorithms and heuristics.
25
Max2SAT
• Instance: A 2CNF formula and a goal K.
• Problem: To decide if there is an assignment
satisfying at least K of ’s clauses. Example: a 2CNF formula
(x | y) (y | z) (x | z) (z | y)
26
26
13
Max2SAT is NP Complete
Theorem: Max2SAT is NP-Complete. Proof: Max2SAT is clearly in NP. We’ll show 3SAT p Max2SAT.
(..|..|..)…(..|..|..) p (..|..)…(..|..) 3SAT Max2SAT
K
27
27
Gadgets
Claim: Let (x,y,z,w) =
(x)(y)(z)(w) (x|y)(y|z)(z|x) (x|w)(y|w)(z|w).
• Every satisfying assignment for (x|y|z) can be extended into an assignment which satisfies exactly 7 of the clauses.
• Other assignments can satisfy at most 6 of the
clauses.
Proof: By truth table on vars.
28
28
14
The Construction
• For each 1im of clauses, replace the i-th clause of the 3CNF formula (||) with a corresponding (,,,xi) to get a 2CNF formula.
• Take K=7m.
Make sure this construction is polynomial
29
29
Correctness
• Every satisfying assignment for the 3CNF formula can be extended into an assignment which satisfies 7m clauses in 2CNF.
• If 7m clauses of the 2CNF formula are satisfied, each clause has 7 satisfied clauses, so the original formula is satisfied.
30
30
15
Conclusion
• 3SATpMax2SAT and Max2SATNP • Max2SAT is NP-Complete.
31
31
2SAT vs 3SAT vs Max2SAT
• We’ve seen that checking if a given CNF formula is satisfiable:
–Polynomial-time decidable, if every clause contains up to 2 literals (2SAT).
–NP-hard, if each clause has up to 3 literals (3SAT).
–NP-hard, if each clause contains up to 2 literals and we look for an optimal solution (Max2SAT).
32
32
16
Solving MaxSAT
• Traditional approaches for MaxSAT:
–Systematic search: check every interpretation to see which interpretation is optimal. It’s complete but has limited scalability
–Local search: randomly start with an interpretation and search its neighborhood for a better one. It’s scalable but sometimes far from optimum (local optimum)
33
33
{(x|y|z; 3), (¬x|y; 2)}
x=1 (y;2) y=0 (;2)
empty clause.
It cannot be satisfied, 2 is necessary cost
Assignments from case-split
We may use case-splits as in DPLL to try all possible interpretations, to find which one is optimal. – This is a systematic search.
34
34
17
Systematic Search: 2 Key Features
The DPLL process, and extensions, for SAT
• Search guided by
– “Well-informed” heuristics
– Clauses falsified or made “critical” during search
• Efficiency relies heavily on the ability to avoid local inconsistencies and prune the search space
• Unit propagation:
if a=0, b=0, and have clause (a or b or c), better force c=1 right away
• Clause learning:
if a search branch reaches a contradiction,
learn why this happened and never let this happen again
35
35
Systematic Search: 2 Key Features
Unfortunately, unit propagation and clause learning are not suitable for case-split MaxSAT solvers.
• Unit resolution is not sound for MaxSAT –S={(p),(p|q),(p|q),(p|r), (p|r),(q|r)}
Using unit resolution, S is simplified to S’: – S’={(p),(q),(q),(r), (r),(q|r)} S’s minimal cost is 1; the cost of S’ is at least 2
• How to assign costs to new clauses?
Systematic MaxSAT solvers are significantly less scalable than systematic SAT solvers
e.g., verification instance cmu-bmc-barrel6.cnf:
– best MaxSAT solvers need 20-30 minutes
– MiniSat needs ~2 seconds
36
36
18
Branch&Bound for Hybrid MaxSAT
proc HyMaxSATBB(H, F, σ, soln)
// return the minimal cost of any interpretation
1 res := BCP(H);
2 if (res = false) return false; // hard causes violated
3 // Assume res = (U, S)
4 σ := σ U;
5 F := simplifySoft(F, σ);
6 if soln lowerBound(F) return soln; // cut by bound
7 A := pickLiteral(S F); // branching on A.
8 if (A = nil) return countFalseClauseWeight(F, σ);
9 soln := min(soln, HyMaxSATBB(S {(A)}, F, σ, soln)); 10 return min(soln, HyMaxSATBB(S {(A)}, F, σ, soln));
37
Branch&Bound: DPLL-like search
Each node is a MaxSAT subproblem We look for the minimal cost solution
(LB) Lower Bound
under estimation of the best solution in the sub-tree
If LBCCthenprune (CC) Current Cost = best solution so far
38
38
19
variables
Illustration: Branch&Bound Search
CC = 0
LB = 6 CC = 2
LB = 5 CC = 4
LB = 3
CC = 5
LB = 3
Solution Found! Cost = 8
Solution = 87 Solution = ∞
CC: Current Cost LB: Lower Bound
CC = 2
LB = 4
CC = 3
LB = 3 Solution Found! Cost = 7
Optimal!
CC = 4
LB = 5
39
Simplification Rules for Soft Clauses
• zero elimination: Weighted clauses with zero
weights can be discarded.
• tautology elimination: Valid clauses are always removed.
• identical merge: Identical clauses are merged into one.
• (α;w1),(α;w2)(α;w1 +w2)
• unit clash: Unit clauses with complement literals can be reduced to one
• (A;w1),(A;w2)(A;w1 -w2),(0;w2)
• weighted resolution
40
20
Weighted Resolution
(x|A;u),(¬x|B;w) where m=min{u,w}
(A | B; m),
(x | A; u-m), (¬x | B; w-m), (x | A | ¬B; m), (¬x | ¬A | B; m)
Example:
(p | q; 2) and (¬p | q; 3) produces 5 clauses:
(q | q; 2), (p | q; 0), (¬p | q; 1), (p | q | ¬q; 2), (p | ¬q | q; 2). which are simplified to (q; 2), (¬p | q; 1).
41
41
Example: Meaning of weighted clauses
(y|z;3), (x|y; 3-3), (x|z; 3-3), (x|y|z; 3), (x|y|z; 3)
x 3
y y x 3 z
z y
y x 3 3 3
x
(x|y; 3), = (x|z; 3)
z z
42
42
21
1 3
Linear Programming (LP) for Low Bound of Hybrid MaxSAT
=
𝑎∧ (C1) ¬𝑎∨𝑏 ∧ (C2) 4: ¬𝑏∨𝑐 ∧ (C3) 2 2: ¬𝑐∨𝑑 ∧ (C4) 7: ¬𝑑 (C5)
Subject to C1 Subject to C2
Minimize
4×C3+2×C4+7×C5
Linear Programming
Integer Programming
Minimize 4×C3+2×C4+7×C5 Subject to a 1,
(1 – a) + b 1, 1–b)+c C3, (1 – c) + d C4,
(1 – d) C5,
0 a, b, c, d, C3, C4, C5 1
Minimize 4×C3+2×C4+7×C5 Subject to a 1,
(1 – a) + b 1, 1–b)+c C3, (1 – c) + d C4,
(1 – d) C5,
a, b, c, d, C3, C4, C5 { 0, 1 }
43
43
Local Search: “Natural” for MaxSAT?
• Local search methods walk on a landscape composed of truth assignments
– Height = number of unsatisfied constraints
• At every point in time, have a (sub-optimal) MaxSAT solution!
– “anytime solution” to MaxSAT
• Bottleneck: local minima, just as in local search for SAT
Ongoing research topics
44
44
22