Microsoft PowerPoint – lecture23 [Compatibility Mode]
COMS4236: Introduction to
Computational Complexity
Spring 2018
Mihalis Yannakakis
Lecture 23, 4/10/18
Quantified Satisfiability – QSAT (or QBF)
• No restriction on # alternations
Input: Quantified Boolean formula in prenex normal form (all
quantifiers at beginning) with no free variables (closed formula)
Q1y1 Q2y2 … Qmym y1,y2,…,ym) where each Qi is a quantifier
( or )
Question: Is the formula true?
• Note: Any formula with quantifiers can be put in prenex
normal form by renaming if necessary some variables and
bringing all the quantifiers to the beginning
• 1. QSAT is in PSPACE
• 2. QSAT is PSPACE-complete
Evaluation of a QBF – Example
0
0
0 0 0
0
0
1
1
1 1 1
1
1
y1
y2
y3
1 2 3 1 2 3 1 2 3 1 2 3y y y .(y y y ) (y y y ) (y y y )
Value of
1 2 3φ(y ,y ,y )
y3.y1,y2,y3)
y2y3.y1,y2,y3)
y1y2y3.y1,y2,y3)
Evaluation of a QBF – Example
1
1 0 11
0 1
0
0
0 0 0
0
0
1
1
1 1 1
1
1
y1
y2
y3
1 2 3 1 2 3 1 2 3 1 2 3y y y .(y y y ) (y y y ) (y y y )
Value of 1 0 0 0 0110
1 2 3φ(y ,y ,y )
y3.y1,y2,y3)
y2y3.y1,y2,y3)
y1y2y3.y1,y2,y3)
QSAT (QBF) is in PSPACE
• Input: F = Q1y1 Q2y2 … Qmym. y1,y2,…,ym)
• Recursive algorithm VAL to evaluate the quantified formula
F with a partial assignment to the first i variables (i.e. is
a bit-vector of length i), i=0,…,m
proc VAL()
if |=m (all variables assigned) then return
else { let i= ||+1;
if Qi = then return VAL(0) VAL(1) (i.e. we call
recursively VAL on extended with 0 for yi, and then
we call it on extended with 1 for yi)
else (Qi = ) return VAL(0) VAL(1)
}
Main: Return VAL() (call VAL on empty assignment)
Recursion Tree
• Full binary tree of depth m, where in each level i we
assign a value to variable yi.
y1
y2 y2
0
0 0
1
11
Every path from root to leaf corresponds to an assignment to
the variables, and at the leaf we evaluate on the assignment
• Depth of the recursion =m = #variables
space needed = m for the recursion stack (the bits of the
partial assignment) + size of for the evaluation of the formula
PSPACE-hardness
• L in PSPACE TM M that decides L with polynomial
space p(n) (and time for some constant c)
• input xÎL path from the initial configuration C0 to the
accepting configuration C* (assume wlog unique)
• Use idea of Savitch’s Theorem
• REACH(C,C’,i):= true iff C can reach C’ in at most steps.
M accepts x iff REACH(C0,C*,cp(n))
• REACH(C,C’,0) iff C=C’ or CC’ (in one move of M)
• REACH(C,C’,i+1) for i≥0 iff
Z. REACH(C,Z,i) REACH(Z,C’,i)
Reason: Take Z = midpoint of the path from C to C’
( )2cp n
2i
Construction of QBF
• Encode configurations in binary (recall proofs of
completeness for Circuit Value and Circuit SAT problems)
• For each i, construct QBF i(Y,Y’) with tuples of free
variables Y,Y’ representing two configurations (formula
includes other quantified variables) such that for all
assignments to Y,Y’
i(Y,Y’) is true iff Y,Y’ encode configurations & REACH(Y,Y’,i)
• Then the final QBF is the closed formula cp(n)(C0,C*) where
we substitute for Y,Y’ the (binary encodings of the) initial
configuration C0, and the accepting configuration C*
• input xÎL cp(n)(C0,C*) true
Construction of i(Y,Y’)
• Basis, 0(Y,Y’): Y=Y’ or Y goes to Y’ in 1 step of M
• Recall from completeness of Circuit Value problem that in a
move of the TM, every bit of the new configuration
(represented by Y’) is a Boolean function of some bits of the
old configuration (represented by Y)
• Include in 0(Y,Y’) subformulas for these equalities relating
the variables of Y’ to the variables of Y
• = can be expressed with , , and
y = y’ iff (y y’) (y y’)
Construction of i(Y,Y’)
• Induction step, i+1(Y,Y’): Zi.i(Y,Zi) i(Zi,Y’)
• If we just use this expression, then length doubles in every
iteration – no good. Want to rewrite so that only one
occurrence of i on the right hand side.
• Introduce additional tuples of variables Ui,Vi
• Zi Ui Vi.[ ( (Ui=Y Vi=Zi) ( Ui=Zi Vi=Y’)) i(Ui,Vi) ]
• = and can be expressed with , , and
eg. […] [( (Ui≠Y Vi≠Zi) ( Ui≠Zi Vi≠Y’)) i(Ui,Vi)]
• Substitute the inductively constructed i(Ui,Vi) on the rhs.
• length(i+1) ≤ length(i)+O(p(n))
• length(cp(n)) = O(p²(n))
Final Quantified Boolean Formula
• Put all the quantification in the beginning so that the
formula is in prenex form. Variables are disjoint, so moving
the quantifiers to the front does not affect the truth of the
formula
• Thus, final formula is of the form (where t=cp(n)):
• Zt Ut Vt Zt-1 Ut-1 Vt-1…. Z0 U0 V0.
[(Ut≠C0 Vt≠Zt) ( Ut≠Zt Vt≠C*)]
[(Ut-1≠Ut Vt-1≠Zt-1) ( Ut-1≠Zt-1 Vt-1≠Vt)]
. . . . .
[ (U0=V0) 1-move-formula(U0,V0) ]
Q3SAT is PSPACE-complete
• Q3SAT: Is a given QBF Q1y1 Q2y2 … Qmym. y1,y2,…,ym)
true, where is a 3CNF formula ?
• Special case of QSAT, so in PSPACE
• Hardness: Reduction from QSAT
• Given Q1y1 Q2y2 … Qmym y1,y2,…,ym) where is an
arbitrary Boolean formula, or even a circuit C, by Cook’s
reduction, we can introduce a new tuple Z of variables for
the gates of the circuit (nodes of the parse tree of the
formula) and construct a 3CNF formula y1,y2,…,ym,Z) s.t.
for every assignment to y1,y2,…,ym :
• y1,y2,…,ym) is true Z. y1,y2,…,ym,Z). Therefore,
• Q1y1…Qmym y1,y2,…,ym) Q1y1…Qmym Z.y1,y2,…,ym,Z).
Q3SAT is PSPACE-complete
• Q3SAT is PSPACE-complete even when restricted to
instances where the quantifiers alternate:
y1 y2 y3 y4 … ym. y1,y2,…,ym)
• Proof: Given a QBF Q1y1 Q2y2 … Qmym. y1,y2,…,ym)
Introduce for each variable yi a new dummy variable y’i
that is quantified in the opposite way, and then in the
prefix put for each pair yi, y’i first the existentially
quantified variable and then the universal. The new
dummy variables don’t appear in
QSAT as a Game
• F = Q1y1 Q2y2 … Qmym y1,y2,…,ym)
• Two players: E, existential player, and U, universal player
• E sets values of the existentially quantified variables
• U sets values of universal variables
• Play takes m rounds (= # variables)
• Round i: If Qi = then Player E chooses a value for yi,
otherwise (Qi =) Player U chooses a value for yi
• Full information: Each player knows what the other player
played in previous rounds.
• If at the end, the selected assignment satisfies then E
wins, otherwise U wins
• QSAT Formula Game: Given formula F, who wins?
Game tree
• Game tree: Tree of all possible moves of both players
• Each internal node labeled by player that moves
• Root-to-leaf paths = possible plays
• In QSAT game, it is = tree of all possible assignments
E
E E EE
U U
0
0
0 0 0
0
0
1
1
1 1 1
1
1
y1
y2
y3
1 2 3 1 2 3 1 2 3 1 2 3y y y .(y y y ) (y y y ) (y y y )Example:
Value of : 1 0 0 0 0110
Strategy and Strategy Tree
• Strategy of a player: Mapping from histories (sequences
of previous decisions of both players) to next decision of
the player (when it is his turn)
• Strategy can be represented by Strategy tree: Subtree of
game tree that picks one edge out of each node labeled
by the player
E
E E EE
U U
0
0
0 0 0
0
0
1
1
1 1 1
1
1
y1
y2
y3
1 2 3 1 2 3 1 2 3 1 2 3y y y .(y y y ) (y y y ) (y y y )
A winning strategy tree of
E player
Value of : 0 0 0 0 0111
QSAT as a Game
• F = Q1y1 Q2y2 … Qmym y1,y2,…,ym)
• E Strategy tree is winning for E if is true at all leaves
• U Strategy tree is winning for U if is false at all leaves
• Player E has a winning strategy iff F is true.
• QSAT Formula Game (Given formula F, which player
wins?) is PSPACE complete
A class of PSPACE Games
• Two-player, full information games
• Competitive games, where one or the other player wins at
the end
• Input x specifies instance of the game
• Polynomial number of rounds
• In each round, one player chooses among a set of choices
– polynomial description of a choice
• At the end, winner is declared by a polynomial-time
function, based on the input and the choices