CS262 Logic and Verification Lecture 9: Satisfiability
CS262 Logic and Verification 1 / 20
Boolean satisfiability problem
Copyright By PowCoder代写 加微信 powcoder
Problem SAT: Given a propositional formula in conjunctive normal form, is there a satisfying assignment for it?
Further questions: If yes, how can we compute it efficiently? If not, how can we prove this?
Example: ⟨[x,y,¬z],[¬x,⊤],[¬y,z,⊥]⟩ = (x ∨y ∨¬z)∧(¬x ∨⊤)∧(¬y ∨z ∨⊥)
W.l.o.g. we may assume that ⊤ or ⊥ do not appear: Eliminate them by neutral element rules [x,⊥] = [x], [x,⊤] = [⊤] = ⊤, ⟨X,⊤⟩ = ⟨X⟩.
Example (continued):
⟨[x, y, ¬z], [¬x, ⊤], [¬y, z, ⊥]⟩ = ⟨[x, y, ¬z], [⊤], [¬y, z]⟩
= ⟨[x, y, ¬z], [¬y, z]⟩
CS262 Logic and Verification
Basic definitions
Definitions:
(positive/negative) literal – a variable, a negated variable clause – disjunction of literals
CNF formula – formula in conjunctive normal form k-CNF formula – every clause has at most k literals k-SAT problem – input of SAT is a k-CNF
CS262 Logic and Verification 3 / 20
Computational complexity
We can solve the problem SAT in time 2n · L by computing the entire truth table, where L is the total number of literals of the input formula, and n is the number of variables.
This problem is the ‘mother’ of all NP-complete problems.
If we could the problem efficiently, i.e., in polynomial time, then many other problems could be solved efficiently as well.
1.000.000$ Millenium prize problem: Is P=NP?
Most likely, there is no efficient algorithm known to solve this problem.
CS262 Logic and Verification
Next steps
Possible approaches from here:
solve special cases efficiently: 2-SAT, Horn formulas
improve the exponential runnning time from 2n to cn for some c < 2
compact reductions: translate problems into SAT problems with small blowup
use SAT solvers and heuristics
CS262 Logic and Verification 5 / 20
Reductions
There is a polynomial time algorithm that, given an instance F of SAT, produces a 3-CNF G(F) such that F is satisfiable if and only if G(F) is satisfiable.
If we can solve 3-SAT efficiently, then we can solve SAT efficiently (in polynomial time).
Consider a clause containing two literals X and Y . Replace X ∨ Y in the clause by a new variable Z (so the clause gets shorter by one literal), and expressX∨Y ≡Z bya3-CNFF(X,Y,Z): [...]
Take the conjunction of the current CNF with F(X,Y,Z). Repeat the process on clauses of length > 3.
CS262 Logic and Verification 6 / 20
Reductions
Problem COLORING: Given a graph G = (V , E ) and integer k , can its vertices be colored properly with k colors?
Definition: A coloring of G is proper, if the end vertices of every edge receive distinct colors.
There is a polynomial time algorithm that, given an instance (G,k) of COLORING, produces a CNF formula F(G,k) such that G has a proper coloring with k colors if and only if F(G,k) is satisfiable.
If we can solve SAT efficiently, then we can solve COLORING efficiently. If we can count the number of satisfying assignment of a CNF formula
efficiently, then we can count proper k-colorings efficiently. A concrete way to tackle a problem with SAT solvers
CS262 Logic and Verification
For each vertex v and each color k, introduce a variable 1 if vertex v receives color k
xv,k = 0 else
Add constraints that every vertex receives exactly one color: […]
Add constraints that the end vertices of every edge receive two distinct colors: […]
Number of variables: |V | · k.
Size of the formula: polynomial in |V| and |E|.
CS262 Logic and Verification
Solving 2-SAT in polynomial time
First method: Resolution
Recall the resolution proof method: maintains a conjunction of disjunctions first step: resolution expansion into CNF second step: resolution rule
Key observation: The resolution rule on clauses of size 2 produces another clause of size ≤ 2. (Example: [x,y],[¬x,¬z] [y,¬z])
At most 1 + 2n + 4n = 2n2 + 1 clauses can ever occur in the process (n 2
is the number of variables).
If formula is unsatisfiable, then the empty clause [ ] will occur; otherwise it is satisfiable.
Hence resolution is a polynomial method for deciding 2-SAT.
CS262 Logic and Verification 9 / 20
A linear-time algorithm for 2-SAT
Recall that
Idea: Capture this implication information of a 2-CNF F in a directed
graph D = D(F):
vertex set V (D ) := V ∪ V , i.e., all variables V = V (F ) and their
negation edge set
E(D) := {(¬u,v),(¬v,u) | [u ∨ v] ∈ F} ∪ {(¬u,u) | [u] ∈ F} 2-clauses lead to two directed edges, whereas a unit clause leads to a
single directed edge.
The graph D has 2n vertices, where n := |V |, and at most 2m edges, where m := |F|.
u ∨ v ≡ ¬u → v ≡ ¬v → u
CS262 Logic and Verification
A linear-time algorithm for 2-SAT
F = ⟨[¬x1, x2], [¬x2, x3], [¬x3, x4], [¬x4, x1], [¬x5, x3], [x5, x1]⟩
F = ⟨[x, y], [¬x, y], [z, ¬y], [¬z, ¬y]]⟩
Definition: Write x y if there is a directed path from x to y in the graph D(F).
CS262 Logic and Verification
A linear-time algorithm for 2-SAT
F is not satisfiable if and only if there is a variable x ∈ V such that x ¬x x.
With this result, satisfiability can be reduced to computing the strongly connected components of the graph D
Definition: Two vertices u and v in a directed graph are strongly connected, if u v and v u. The strongly connected components are the maximal subsets of vertices with this property.
The strongly connected components of a directed graph can be computed in linear time in the size of the graph, i.e., in time that is linear in the number of vertices and edges, by well-known standard graph algorithms.
CS262 Logic and Verification 12 / 20
A linear-time algorithm for 2-SAT
F is not satisfiable if and only if there is a variable x ∈ V such that x ¬x x.
Proof: Let F′ denote the CNF obtained from F by exhaustively applying the resolution rule.
Consider the resolvent [u,v] of [x,u] and [¬x,v]. This resolvent would add two new edges to the graph, namely ¬u → v and ¬v → u. But the edges ¬u → x → v and ¬v → ¬x → u were already present. So adding these edges does not alter the relation .
F is not satisfiable ⇐⇒
[]appearsinF′ ⇐⇒
[x],[¬x] appears in F′ for some variable x ∈ V ⇐⇒ x → ¬x → x in D(F′) ⇐⇒
x ¬x x in D(F).
CS262 Logic and Verification
Applications to 3-Satisfiability
Idea: Want to use our polynomial-time algorithms for solving 2-SAT for solving 3-SAT more efficiently, i.e., in less than 2n steps (n is the number of variables).
Definition: Given a 3-CNF F over n variables. A subset G of clauses of F is called independent, if no two clauses share any variables. We consider such a subset G of maximal size, i.e., no further clauses can be added without violating independence.
Example: F =⟨[a,b,¬c],[c,¬d,e],[¬e,f,g],[¬f,g,¬h],[h,i,¬j]⟩ G =⟨[a,b,¬c],[¬e,f,g],[h,i,¬j]⟩
G′ =⟨[c,¬d,e],[¬f,g,¬h]⟩
CS262 Logic and Verification
Applications to 3-Satisfiability
Consider a maximal set G of independent 3-clauses in F. Then we have |G| ≤ n/3.
For any truth assignment α to the variables in G, F[α] is a 2-CNF. Here, F[α] is the formula obtained from F by setting all variables defined by α to true or false (remove clauses with true literals and remove false literals from clauses).
The number of truth assignments satisfying G is 7|G| ≤ 7n/3. Proof: […]
CS262 Logic and Verification
Algorithm for 3-SAT
Algorithm: Go through all truth assignments α satisfying G, and check satisfiability of the 2-CNF F[α] in polynomial time (quadratic or linear).
Satisfiability of a 3-CNF formula can be decided in time O(7n/3poly(n)) = O(1.913n).
CS262 Logic and Verification 16 / 20
Horn satisfiabiliy
We saw that 2-SAT is a special case of SAT that can be solved efficiently
We now consider another special case, where there is no restriction on the size of clauses, but on their structure
Definition: A Horn clause is a clause in which there is at most one positive literal (non-negated variable)
A Horn CNF is a CNF that has only Horn clauses. Examples:
[¬x , ¬y , ¬z , a] = ¬x ∨ ¬y ∨ ¬z ∨ a = (x ∧ y ∧ z ) → a [¬x, ¬y, ¬z]
CS262 Logic and Verification
Horn clauses in statements are Horn clauses.
The clause [¬x , ¬y , ¬z , a] = (x ∧ y ∧ z ) → a is written as: a :- x, y, z.
CS262 Logic and Verification 18 / 20
Satisfiability of Horn CNFs
Here are some simple observations:
If F = ⟨ ⟩, then F is satisfied by any assignment.
If every clause has size ≥ 2, then the formula can be satisfied by setting all variables to false.
If the formula has a clause of size = 1, then we have to set the literal in this clause to true to satisfy the formula.
If the formula contains the empty clause [ ], then the formula is not satisfiable.
CS262 Logic and Verification 19 / 20
A linear-time algorithm
These observations give the following algorithm:
Input: Horn CNF F
Output: ‘Yes’ if F is satisfiable, ‘No’ if F is not satisfiable while ([ ] ̸∈ F) {
IfF =⟨⟩oreveryclauseinF hassize≥2,return‘Yes’ Pickaclause[u]∈F ofsize=1.
Remove all clauses containing u from F, and
remove the literal ¬u from all clauses containing it. }
return ‘No’
Example: F = ⟨[¬y, ¬x, z], [¬y, z], [¬z], [¬z, x]⟩
This algorithm decides satisfiability of a Horn CNF in linear time.
CS262 Logic and Verification
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com