CS/ECE 374: Algorithms & Models of
Computation
More on SAT
Lecture 23
Circuits
Definition
A circuit is a directed acyclic graph with
1 ? ? 0 ?∧ ∨ ∨¬ ∧∧Inputs:Output:
1 Input vertices (withoutincoming edges) labelled with
0, 1or a distinct variable.2 Every other vertex is labelled
∨, ∧or ¬.
3 Single node output vertex
Circuits
Definition
A circuit is a directed acyclic graph with
1 ? ? 0 ?∧ ∨ ∨¬ ∧∧Inputs:Output:
1 Input vertices (withoutincoming edges) labelled with
0, 1or a distinct variable.2 Every other vertex is labelled
∨, ∧or ¬.
3 Single node output vertex
Circuits
Definition
A circuit is a directed acyclic graph with
1 ? ? 0 ?
∧ ∨ ∨
¬ ∧
∧
Inputs:
Output: 1 Input vertices (without
incoming edges) labelled with
0, 1or a distinct variable.2 Every other vertex is labelled
∨, ∧or ¬.
3 Single node output vertex
CSAT: Circuit Satisfaction
Definition (Circuit Satisfaction (CSAT).)
Given a circuit as input, is there an assignment to the input variablesthat causes the output to get value1?
Claim
CSAT is inNP.
1 Certificate: Assignment to input variables.
2 Certifier: Evaluate the value of each gate in a topological sort of
CSAT: Circuit Satisfaction
Definition (Circuit Satisfaction (CSAT).)
Given a circuit as input, is there an assignment to the input variablesthat causes the output to get value1?
Claim
CSAT is inNP.
1 Certificate: Assignment to input variables.
2 Certifier: Evaluate the value of each gate in a topological sort of
Circuit SAT vs SAT
CNF formulas are a rather restricted form of Boolean formulas.Circuits are a much more powerful (and hence easier) way to expressBoolean formulas
However they are equivalent in terms of polynomial-time solvability.
Theorem
SAT≤P 3SAT ≤P CSAT.
Theorem
Circuit SAT vs SAT
CNF formulas are a rather restricted form of Boolean formulas.Circuits are a much more powerful (and hence easier) way to expressBoolean formulas
However they are equivalent in terms of polynomial-time solvability.
Theorem
SAT≤P 3SAT ≤P CSAT.
Theorem
Converting a
CNF
formula into a Circuit
Given3CNF formulat ϕ with n variables and m clauses, create a
CircuitC.
Inputs toC are the n boolean variables x1, x2, . . . , xnUse NOT gate to generate literal ¬xi for each variable xiFor each clause (`1 ∨ `2∨ `3) use two OR gates to mimicformula
Converting a circuit into a
CNF
formula
Label the nodes
1 ? ? 0 ?InputsOutput:∧∧∧∨ ∨¬1,a ?,b ?,c 0,d ?,eInputsOutput: ∧, k¬, i ∧, j∧, f ∨, g ∨, h
Converting a circuit into a
CNF
formula
Introduce a variable for each node
1,a ?,b ?,c 0,d ?,eInputsOutput: ∧, k¬, i ∧, j∧, f ∨, g ∨, h1,a ?,b ?,c 0,d ?,eInputsOutput: ∧, k¬, i ∧, j∧, f ∨, g ∨, hxkxjxixf xg xhxa xb xc xd xe
Converting a circuit into a
CNF
formula
Write a sub-formula for each variable that is true if the var is computedcorrectly.1,a ?,b ?,c 0,d ?,eInputsOutput: ∧, k¬, i ∧, j∧, f ∨, g ∨, hxkxjxixf xg xhxa xb xc xd xe
xk (Demand a sat’ assignment!)
xk = xi ∧ xjxj = xg ∧ xhxi = ¬xfxh = xd ∨ xexg = xb∨ xcxf = xa ∧ xbxd = 0xa = 1
(C) Introduce var for each node.
Converting a circuit into a
CNF
formula
Convert each sub-formula to an equivalentCNFformula
Converting a circuit into a
CNF
formula
Take the conjunction of all theCNFsub-formulas
1,a ?,b ?,c 0,d ?,eInputsOutput: ∧, k¬, i ∧, j∧, f ∨, g ∨, hxkxjxixf xg xhxa xb xc xd xexk ∧ (¬xk ∨ xi) ∧ (¬xk ∨ xj)∧ (xk∨ ¬xi ∨ ¬xj) ∧ (¬xj∨ xg)∧ (¬xj∨ xh) ∧ (xj∨ ¬xg∨ ¬xh)∧ (xi ∨ xf) ∧ (¬xi ∨ ¬xf)∧ (xh ∨ ¬xd) ∧ (xh ∨ ¬xe)∧ (¬xh∨ xd ∨ xe) ∧ (xg ∨ ¬xb)∧ (xg ∨ ¬xc) ∧ (¬xg ∨ xb ∨ xc)∧ (¬xf ∨ xa) ∧ (¬xf ∨ xb)∧ (xf ∨ ¬xa∨ ¬xb) ∧ (¬xd) ∧ xaWe got aCNF formula that is satisfiable if and only if the original
Reduction:
CSAT
≤
P
SAT
1 For each gate (vertex) v in the circuit, create a variablexv
2 Case ¬: v is labeled ¬and has one incoming edge from u (so
xv = ¬xu). In SATformula generate, add clauses (xu ∨ xv),
(¬xu ∨ ¬xv). Observe that
xv = ¬xu is true ⇐⇒
(xu ∨ xv)
(¬xu ∨ ¬xv)
Reduction:
CSAT
≤
P
SAT
Continued...
1 Case ∨: So x
v = xu ∨ xw. In SATformula generated, add
Reduction:
CSAT
≤
P
SAT
Continued...
1 Case ∧: So x
v = xu ∧ xw. In SATformula generated, add
Reduction:
CSAT
≤
P
SAT
Continued...
1 If v is an input gate with a fixed value then we do the following.If xv = 1 add clause xv. If xv = 0 add clause ¬xv
Correctness of Reduction
Need to show circuitC is satisfiable iff ϕC is satisfiable
⇒ Consider a satisfying assignment afor C
1 Find values of all gates in C undera
2 Give value of gate v to variable xv; call this assignmenta03 a0 satisfiesϕC (exercise)
⇐ Consider a satisfying assignment afor ϕC
Part II
SAT
≤
P
3SAT
How SAT is different from 3SAT?
InSAT clauses might have arbitrary length: 1, 2, 3, . . . variables:
x ∨ y ∨ z ∨ w ∨ u∧¬x ∨ ¬y ∨ ¬z ∨ w ∨ u∧¬x
In3SAT every clause must have exactly 3different literals.
To reduce from an instance of SAT to an instance of 3SAT, we
must make all clauses to have exactly 3variables...
Basic idea
1 Pad short clauses so they have 3literals.2 Break long clauses into shorter clauses.
SAT
≤
P
3SAT
How SAT is different from 3SAT?
InSAT clauses might have arbitrary length: 1, 2, 3, . . . variables:
x ∨ y ∨ z ∨ w ∨ u∧¬x ∨ ¬y ∨ ¬z ∨ w ∨ u∧¬x
In3SAT every clause must have exactly 3different literals.
To reduce from an instance of SAT to an instance of 3SAT, we
must make all clauses to have exactly 3variables...
Basic idea
1 Pad short clauses so they have 3literals.2 Break long clauses into shorter clauses.
3SAT
≤
P
SAT
1 3SAT ≤
P SAT.
2 Because...
SAT
≤
P
3SAT
Claim
SAT≤P 3SAT.
Givenϕ a SATformula we create a 3SAT formula ϕ0 such that
1 ϕ is satisfiable iff ϕ0 is satisfiable.
2 ϕ0 can be constructed from ϕ in time polynomial in|ϕ|.
SAT
≤
P
3SAT
Claim
SAT≤P 3SAT.
Givenϕ a SATformula we create a 3SAT formula ϕ0 such that
1 ϕ is satisfiable iff ϕ0 is satisfiable.
2 ϕ0 can be constructed from ϕ in time polynomial in|ϕ|.
SAT
≤
P
3SAT
Claim
SAT≤P 3SAT.
Givenϕ a SATformula we create a 3SAT formula ϕ0 such that
1 ϕ is satisfiable iff ϕ0 is satisfiable.
2 ϕ0 can be constructed from ϕ in time polynomial in|ϕ|.
SAT
≤
P
3SAT
A clause with two literals
Reduction Ideas: clause with 2 literals1 Case clause with 2 literals: Letc = `
1 ∨ `2. Let u be a newvariable. Considerc0 = `1 ∨ `2 ∨ u∧ `1 ∨ `2 ∨ ¬u.
2 Supposeϕ = ψ ∧ c. Then ϕ0 = ψ ∧ c0 is satisfiable iff ϕ is
SAT
≤
P
3SAT
A clause with a single literal
Reduction Ideas: clause with 1 literal
1 Case clause with one literal: Letc be a clause with a singleliteral (i.e., c = `). Let u, v be new variables. Consider
c0 = ` ∨ u ∨ v∧` ∨ u ∨ ¬v
∧` ∨ ¬u ∨ v∧` ∨ ¬u ∨ ¬v.
2 Supposeϕ = ψ ∧ c. Then ϕ0 = ψ ∧ c0 is satisfiable iff ϕ is
SAT
≤
P
3SAT
A clause with more than 3 literals
Reduction Ideas: clause with more than 3 literals1 Case clause with five literals: Let c = `
1∨ `2 ∨ `3∨ `4 ∨ `5.
Letu be a new variable. Consider
c0 = `1∨ `2 ∨ `3∨ u
∧ `4∨ `5 ∨ ¬u
.
2 Supposeϕ = ψ ∧ c. Then ϕ0 = ψ ∧ c0 is satisfiable iff ϕ is
SAT
≤
P
3SAT
A clause with more than 3 literals
Reduction Ideas: clause with more than 3 literals1 Case clause with k > 3literals: Let c = `
1 ∨ `2∨ . . . ∨ `k.
Letu be a new variable. Consider
c0 = `1 ∨ `2. . . `k−2 ∨ u
∧ `k−1 ∨ `k∨ ¬u
.
2 Supposeϕ = ψ ∧ c. Then ϕ0 = ψ ∧ c0 is satisfiable iff ϕ is
Breaking a clause
Lemma
For any boolean formulas X and Y and z a new boolean variable.
Then
X ∨ Y is satisfiable
if and only if,z can be assigned a value such that
X ∨ z∧Y ∨ ¬z is satisfiable
SAT
≤
P
3SAT
(contd)
Clauses with more than 3 literals
Letc = `1 ∨ · · · ∨ `k. Let u1, . . . uk−3 be new variables. Consider
c0 = `1 ∨ `2∨ u1∧ `3∨ ¬u1 ∨ u2∧ `4 ∨ ¬u2 ∨ u3∧· · · ∧ `k−2 ∨ ¬uk−4 ∨ uk−3∧ `k−1∨ `k ∨ ¬uk−3.Claim
ϕ = ψ ∧ c is satisfiable iffϕ0 = ψ ∧ c0 is satisfiable.Another way to see it — reduce size of clause by one:
c0 =`1 ∨ `2. . . ∨ `k−2∨ uk−3
∧`k−1 ∨ `k ∨ ¬uk−3
Overall Reduction Algorithm
Reduction from SAT to 3SAT
ReduceSATTo3SAT(ϕ):
// ϕ: CNF formula.
for each clause c of ϕ do
if c does not have exactly 3 literals then
construct c0 as before
else
c0= c
ψ is conjunction of all c0 constructed in loop
return Solver3SAT(ψ)
Correctness (informal)
Part III
Power of SAT and CSAT
SATand CSAT are meta-problems
Allow us to express/model problem using constraints. In essense theyallow programming with constraints of certain restricted type.
Reduce Directed Hamilton Path to SAT
Given directed graph G = (V , E ), does it have a Hamilton path?
GivenG obtain CNF formula ϕG such that G has a Hamilton Path
iff ϕG is satisfiable
Alternative view: Program/express using constraintsWhat are variables?
What are the constraints?
One approach: G has a Hamilton path iff there is a permutation of
the n vertices such that for each i there is an edge from vertex inposition i to vertex in position (i + 1)
Reduce Directed Hamilton Path to SAT
Given directed graph G = (V , E ), does it have a Hamilton path?
GivenG obtain CNF formula ϕG such that G has a Hamilton Path
iff ϕG is satisfiable
Alternative view: Program/express using constraintsWhat are variables?
What are the constraints?
One approach: G has a Hamilton path iff there is a permutation of
the n vertices such that for each i there is an edge from vertex inposition i to vertex in position (i + 1)
Reduce Directed Hamilton Path to SAT
Given directed graph G = (V , E ), does it have a Hamilton path?
GivenG obtain CNF formula ϕG such that G has a Hamilton Path
iff ϕG is satisfiable
Alternative view: Program/express using constraintsWhat are variables?
What are the constraints?
One approach: G has a Hamilton path iff there is a permutation of
Reduction continued
Define variablex (u, i ) if vertex u in position i in the permutation.Total of n2 variables where n = |V |.
Constraints?
For eachu, exactly one of x (u, 1), x (u, 2), . . . , x (u, n) shouldbe true
Wn
i =1x (u, i ) to ensure that x (u, i ) is1 for at least onei
Fori 6= j we add constraint ¬x(u, i ) ∨ ¬x(u, j )to ensure thatwe cannot choose both to be 1 for any pair.
For eachu we have a total of(1 + n(n − 1)/2) constraints.Total of n(1 + n(n − 1)/2)over all vertices.
x (u, i )and x (v , i + 1) implies edge (u, v ) in E (G )(x (u, i ) ∧ x (v , i + 1)) ⇒ z (u, v )where z(u, v )is 1 if
Reduction continued
Define variablex (u, i ) if vertex u in position i in the permutation.Total of n2 variables where n = |V |.
Constraints?
For eachu, exactly one of x (u, 1), x (u, 2), . . . , x (u, n) shouldbe true
Wn
i =1x (u, i ) to ensure that x (u, i ) is1 for at least onei
Fori 6= j we add constraint ¬x(u, i ) ∨ ¬x(u, j )to ensure thatwe cannot choose both to be 1 for any pair.
For eachu we have a total of (1 + n(n − 1)/2) constraints.Total of n(1 + n(n − 1)/2)over all vertices.
x (u, i )and x (v , i + 1) implies edge (u, v ) in E (G )
(x (u, i ) ∧ x (v , i + 1)) ⇒ z (u, v )where z(u, v )is 1 if
Reduction continued
Define variablex (u, i ) if vertex u in position i in the permutation.Total of n2 variables where n = |V |.
Constraints?
For eachu, exactly one of x (u, 1), x (u, 2), . . . , x (u, n) shouldbe true
Wn
i =1x (u, i ) to ensure that x (u, i ) is1 for at least onei
Fori 6= j we add constraint ¬x(u, i ) ∨ ¬x(u, j )to ensure thatwe cannot choose both to be 1 for any pair.
For eachu we have a total of (1 + n(n − 1)/2) constraints.Total of n(1 + n(n − 1)/2)over all vertices.
Vertex Cover to CSAT
Given graphG = (V , E ) and integer k, doesG have a vertex cover
of size at most k?
RecallS ⊆ V is a vertex cover if each edge (u, v ) is covered by S,
that meansu ∈ S or v ∈ S.
How do we reduce to CSAT/SAT? What are the variables?
xu, u ∈ V to indicate whether we choose uConstraints?
For each edge(u, v ) ∈ E a constraint (xu ∨ xv). Total of |E |constraints.
P
Vertex Cover to CSAT
Given graphG = (V , E ) and integer k, doesG have a vertex cover
of size at most k?
RecallS ⊆ V is a vertex cover if each edge (u, v ) is covered by S,
that meansu ∈ S or v ∈ S.
How do we reduce to CSAT/SAT? What are the variables?
xu, u ∈ V to indicate whether we choose u
Constraints?
For each edge(u, v ) ∈ E a constraint (xu ∨ xv). Total of |E |constraints.
P
Vertex Cover to CSAT
Given graphG = (V , E ) and integer k, doesG have a vertex cover
of size at most k?
RecallS ⊆ V is a vertex cover if each edge (u, v ) is covered by S,
that meansu ∈ S or v ∈ S.
How do we reduce to CSAT/SAT? What are the variables?
xu, u ∈ V to indicate whether we choose uConstraints?
For each edge(u, v ) ∈ E a constraint (xu ∨ xv). Total of |E |constraints.
P
Vertex Cover to CSAT
Given graphG = (V , E ) and integer k, doesG have a vertex cover
of size at most k?
RecallS ⊆ V is a vertex cover if each edge (u, v ) is covered by S,
that meansu ∈ S or v ∈ S.
How do we reduce to CSAT/SAT? What are the variables?
xu, u ∈ V to indicate whether we choose uConstraints?
For each edge(u, v ) ∈ E a constraint (xu ∨ xv). Total of |E |constraints.
P
Vertex Cover to CSAT
Given graphG = (V , E ) and integer k, doesG have a vertex cover
of size at most k?
RecallS ⊆ V is a vertex cover if each edge (u, v ) is covered by S,
that meansu ∈ S or v ∈ S.
How do we reduce to CSAT/SAT? What are the variables?
xu, u ∈ V to indicate whether we choose uConstraints?
For each edge(u, v ) ∈ E a constraint (xu ∨ xv). Total of |E |constraints.
P
Vertex Cover to CSAT
Expressing P
u∈Vxu ≤ k as a circuit.
Given inputsxu, u ∈ V can create an addition circuit that
outputs the sumP
uxu as a dlog nebit binary number
Given twor-bit binary inputs y1, y2, . . . , yr and z1, z2, . . . , zrone can develop a boolean circuit to compare which one isgreater
Hence circuit to do P
uxu and compare output to input integer
k written in binary
Vertex Cover to CSAT
Expressing P
u∈Vxu ≤ k as a circuit.
Given inputsxu, u ∈ V can create an addition circuit that
outputs the sumP
uxu as a dlog nebit binary number
Given twor-bit binary inputs y1, y2, . . . , yr and z1, z2, . . . , zrone can develop a boolean circuit to compare which one isgreater
Hence circuit to do P
uxu and compare output to input integer
k written in binary
Cook-Levin Theorem
Theorem (Cook-Levin)
SATis NP-Complete.
How did they prove it? And why SATor CSAT?
Proof is in retrospect simple.
Fix any non-deterministic TM M and string w
Does M accept w in p(|w |)steps where p() is some fixed
polynomial?
Can express computation of M on w using a polynomial sized
Mathematical Programming
SAT, CSAT are boolean constraint satisfaction problems.
Other frameworks: constraints involving linear inequalities, convexfunctions, polynomials etc
Useful to know: Integer Linear Programming (ILP), LinearProgramming (LP), Mixed Integer Linear Programming (MIP),Convex Programming
Linear Programming
Problem
Real variablesx1, x2, . . . , xn. Solve
maximize/minimize Pnj =1cjxjsubject to Pnj =1aijxj ≤ bi for i = 1 . . . pPnj =1aijxj = bi for i = p + 1 . . . qPnj =1aijxj ≥ bi for i = q + 1 . . . mInput is matrix A = (aij) ∈ Rm×n, column vector b = (bi) ∈ Rm,and row vectorc = (cj) ∈ Rn
Integer Linear Programming
Problem
Integer variablesx1, x2, . . . , xn. Solve
maximize/minimize Pnj =1cjxjsubject to Pnj =1aijxj ≤ bi for i = 1 . . . pPnj =1aijxj = bi for i = p + 1 . . . qPnj =1aijxj ≥ bi for i = q + 1 . . . nxi ∈ Z for i = 1 to d
Input is matrix A = (aij) ∈ Rm×n, column vector b = (bi) ∈ Rm,and row vectorc = (cj) ∈ Rn
Convex Programming
Problem
Real variablesx1, x2, . . . , xn. x ∈ Rn Solve
minimize f (x )
subject to gi(x ) ≤ bi for i = 1 . . . m
Mathematical Programming
LP is a specical case of Convex ProgrammingLP can be solved in polynomial time
Convex programs can be solved arbitrarily well in polynomialtime (exact solution is tricky because of irrational solutions)ILP and MIP are NP-Hard (decision versions are NP-Complete).
Why is convex programming solvable?
For convex programs, local optimum is a global optimum!Local optimum can be found by local search! Gradient descent!Even for non-convex programs
Mathematical Programming
LP is a specical case of Convex ProgrammingLP can be solved in polynomial time
Convex programs can be solved arbitrarily well in polynomialtime (exact solution is tricky because of irrational solutions)ILP and MIP are NP-Hard (decision versions are NP-Complete).Why is convex programming solvable?
For convex programs, local optimum is a global optimum!Local optimum can be found by local search! Gradient descent!Even for non-convex programs
Interplay of Discrete and Continuous
Optimization
Both are fundamental and important and interplay has lot of impact!Machine learning: (deep) learning uses continuous optimizationto train neural networks for classification and other discrete tasksCombinatorial optimization: use LP/SDP and other convexprogramming methods to solve combinatorial problemsScientific and numerical computing
Statistics
