pptx

Report
U N I V E R S I T Y
O F
B E R G E N
Algorithms Research Group
New developments in Circuit Complexity
From Circuit-SAT Algorithms to Circuit Lower Bounds
Bart M. P. Jansen
University of Bergen, Norway
uib.no
March 20th 2014, UiB Algorithms Group Winter School
2014
Algorithms Research Group
Circuit complexity up to 2010
• 1970’s:
– Boolean circuits are combinatorial objects
• Possibly easier to understand than Turing machines
– Analyze circuits to separate P from NP?
– If P ≠ NP is there a large program that solves SAT instances of size ≤ 106?
• Non-uniform circuit lower bounds exclude this possibility
• Early 1980’s: Parity does not have non-uniform poly-size AC0 circuits
– What happens if we give AC0 the parity function for free?
– Study AC0 with mod 2 gates of arbitrary fan-in
• Late 1980’s: Majority does not have non-uniform poly-size AC0[2] circuits
– What happens if we give an arbitrary constant mod gate for free?
• 1989: Barrington conjectures:
– Majority does not have non-uniform poly-size AC0[m] circuits for fixed m
• 1990’s: Prove NEXP does not have non-uniform poly-size AC0[m] circuits?
– Open until 2010
2
uib.no
Algorithms Research Group
A solution to an embarrassing problem
• STOC 2010, Ryan Williams:
– “Improving exhaustive search implies superpolynomial lower bounds”
– Improvements over brute force for Circuit-SAT yield superpolynomial
Boolean circuit lower bounds for NEXP
• CCC 2011, Ryan Williams:
– “Non-uniform ACC Circuit Lower Bounds”
– Improvements over brute force for ACC-Circuit-SAT yield
superpolynomial nonuniform ACC circuit lower bounds for NEXP
– Such improvements are possible by exploiting the structure of ACC
• NEXP does not have poly-size non-uniform ACC circuits
3
uib.no
Algorithms Research Group
Goal of this lecture
• Informally:
NEXP ⊄ ACC
• (More) Formally:
There is a language in NEXP that is not decided by a family of constant-depth,
polynomial-size circuits using AND/OR/NOT/MOD[m] gates of unbounded fan-in
• (Even more) Formally:
∃L ∈ NEXP: ¬ (
∃d,m ∈ ℕ, ∃ polynomial p, ∃ circuit family C1, C2, ... such that:
Cn is a circuit of size ≤ p(n) of depth ≤ d over gateset
{AND,OR,NOT,Mod[m]} that decides all n-bit inputs of L
)
4
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
Testing poly(n)-size ACC
circuits with n inputs for

satisfiability in 2 − time
II. Nontrivial ACC-Circuit-SAT algorithms exist
a. Decomposing ACC circuits using
multilinear polynomials
b. Quickly evaluating a multilinear
polynomial on many points
c. Reducing the number of variables
NEXP ⊄ ACC
5
uib.no
Algorithms Research Group
Approaching the problem
• We are proving size lower bounds for non-uniform circuits
– You are allowed “infinite time” to design the ideal circuit to
solve n-bit instances
– Still, no polynomial-size circuit family will solve all instances
• The lower bound is unconditional
– Does not rely on P ≠ NP, ETH, Unique Games, etc.
• Where to start?!
– Non-deterministic time hierarchy theorem:
• If   + 1 ∈ (()), then NTIME[f(n)] ⊂ NTIME[g(n)]
• Unconditionally, strict subset
• Proof by contradiction: assume both [A] NEXP ⊆ ACC and [B]
nontrivial ACC-Circuit-SAT, then contradict time hierarchy theorem
6
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
(ACC-Circuit-SAT in time
c. Checking an
assignment by
analyzing a circuit


−
2
)
∧ (NEXP ⊆ ACC)
¬ (Non-det. time hierarchy theorem)
7
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
⇒
⇒⊥
uib.no
Algorithms Research Group
Contradicting the time hierarchy theorem
• How to speed up all problems in NTIME[2]?
– Give an improvement for a NEXP-complete problem
• Which problem to pick?
– Succinct 3SAT
– (It is “very very NEXP-complete”)
• Let TT(C) denote the length-2 bitstring you get by
– evaluating an -input circuit C
– on all -bit strings
– in lexicographical order
•
8
TT(C)=C(000…000) C(000…001) C(000…010) … C(111…111)
uib.no
Algorithms Research Group
Succinct 3SAT
• Succinct 3SAT is the following problem:
– Input: A Boolean circuit 
– Question: Does TT() encode a satisfiable 3SAT formula?
• Succinct 3SAT is NEXP-complete under poly-time reductions
• A -bit string encodes a formula with  variables and  clauses
– A literal  =  or  = ¬ in a clause (1 ∨ 2 ∨ 3) is encoded by
• Sign bit for possible negation
• -bit binary encoding of variable index 
– Encoding length of a clause is 3( + 1)
• In a
2-bit
string, we can encode
2
3 +1
clauses
• Define remaining clauses to be trivially true (1 ∨ ¬ 1 ∨ 1)
– Given , easy to determine which 3( + 1) bits encode ith clause
9
uib.no
Algorithms Research Group
Ryan’s intuition
•
If NEXP (and therefore Succinct 3SAT) has small ACC
circuits, then this shows a “weakness” of Succinct 3SAT
– A poly(n)-size circuit for the n-bit instances
compresses the yes/no answers to all 2n n-bit
instances into poly(n) bits
•
This weakness should also be exploitable algorithmically
– If NEXP has small ACC circuits, Succinct 3SAT should
be solvable better than brute force, contradicting the
time hierarchy theorem
“At this point we have reached a degree of handwaving so
exuberant, one may fear we are about to fly away. Surprisingly,
this handwaving has a completely formal theorem behind it.”
(Ryan Williams 2011, SIGACT News)
10
uib.no
Algorithms Research Group
Efficient Cook-Levin for NEXP
• For each L ∈ NTIME[2], there is a polynomial-time reduction
R from L to Succinct 3SAT such that:
–  ∈  ⇔ () ∈ Succinct 3SAT
• ( is a yes-instance iff () is a circuit  where TT(C)
encodes a satisfiable 3SAT formula)
– () is a circuit with (||) gates
– For long enough x, () has at most || + 4 log || inputs
• Follows from prior work, e.g., Fortnow, Lipton, van
Melkebeek, Viglas ’05
11
uib.no
Algorithms Research Group
Time lower bound for Succinct 3SAT
• Theorem. Succinct 3SAT on a circuit  with  inputs and size


−
poly() cannot be solved in NTIME[2
]
• Proof. Suppose this is possible, let L ∈ NTIME[2]
• To decide an n-bit instance  of L in NTIME[(2)] :
– Compute equivalent Succinct 3SAT instance
• A circuit  ∶= () of size () on  + 4 log  inputs
– Apply hypothetical Succinct 3SAT algorithm to 
– Runtime is:

2 +4 log  − +4 log  ≤

2− +4 log    ≤  2
• Contradiction to non-det. time hierarchy theorem
12
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
(ACC-Circuit-SAT in time


−
2
)
-input Succinct 3SAT in


−
NTIME[2
]
∧ (NEXP ⊆ ACC)
¬ (Non-det. time hierarchy theorem)
13
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
⇒
⇒
⇒⊥
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
14
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
uib.no
Algorithms Research Group
Consequences of NEXP ⊆ ACC
• Exploit assumption [A]: NEXP ⊆ ACC
• [A] ⇒ poly-size ACC circuits for Succinct 3SAT
– For every , satisfiability of the 3SAT formula encoded by a
bitlength- circuit can be determined by a poly()-size ACC
circuit
• Impagliazzo, Kabanets, Wigderson ‘02 boosts this to:
• [A] ⇒ poly-size Boolean circuits encoding satisfying assignments
– ∀ Boolean circuits :
formula TT() is satisfiable ⇒
∃ poly(||)-size circuit  encoding satisfying assignment
– Assignment setting  to () satisfies TT(C)
15
uib.no
Algorithms Research Group
Exploiting small witness circuits
• We are building a nondeterministic algorithm using [A]
• Guess the circuit W encoding the satisfying assignment?
– Solve Succinct 3SAT instance  as follows:
• Guess a small circuit 
• Answer yes if TT() satisfies TT()
– Under [A] this is a correct nondeterministic algorithm
• How to verify that TT() satisfies TT()?
– If  has  inputs, writing down the formula of size 2 and


−

manipulating it requires 2 time, we need 2
• Use the ACC Circuit SAT algorithm?
16
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
17
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
uib.no
Algorithms Research Group
Checking a guessed assignment using Circuit SAT
•
TT(W) satisfies TT(C)  impossible to pick 
•
By making () copies of the -input circuit , we can get
– an -input, multi-output circuit ’ of poly(||) size,
– on input , circuit ’ outputs the 3( + 1) bits of the  th clause
18
such that no literal of the  th clause is satisfied by TT(W)
uib.no
Algorithms Research Group
Checking a guessed assignment using Circuit SAT
•
TT(W) satisfies TT(C)  impossible to pick 
•
Compose ’ with three copies of  to obtain circuit 
– Feed the indices of the variables in clause  to a copy of  to find the truth value
– Clause  is satisfied if the sign bit of one of the literals matches the truth value under 
19
such that no literal of the  th clause is satisfied by TT(W)
uib.no
Algorithms Research Group
Checking a guessed assignment using Circuit SAT
•
TT(W) satisfies TT(C)  impossible to pick 
•
Assignment encoded by  satisfies formula encoded by  iff () = 1 for all possible clauses
20
such that no literal of the  th clause is satisfied by TT(W)
uib.no
Algorithms Research Group
Checking a guessed assignment using Circuit SAT
•
TT(W) satisfies TT(C)  ¬D is unsatisfiable
•
D has  inputs: run a circuit SAT algorithm on ¬D to determine whether the guess was correct!

– Circuit SAT in 2− time for -input, poly() size circuits would solve -input, poly()-size
Succinct 3SAT instance fast enough to contradict the time hierarchy theorem
Problem:
¬D is not an ACC circuit
(depth may be large)
Solution:
Replace W and C’ by
ACC circuits
21
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
22
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
uib.no
Algorithms Research Group
Equivalent ACC circuits for every Boolean circuit
• Assume [A]: NEXP ⊆ ACC
• Consider the meta-algorithmic Circuit Value problem:
– Input: Binary encoding  of -input circuit , bitstring ’ ∈ {0,1}
– Question: Does  output 1 on input ’?
• Circuit Value is in P (given the input, simulate the circuit)
– So Circuit Value ∈ P (⊆ NEXP) has poly-size ACC circuits by [A]
Constant-depth
ACC circuit of
size poly( + ’)
Binary encoding of a circuit 
23
Value of (’)
Input ’
uib.no
Algorithms Research Group
Equivalent ACC circuits for every Boolean circuit
• Consider an -input poly()-size Boolean circuit 
– Hardcode  into a Circuit Value Decider of size poly()
– Yields a poly()-size ACC circuit equivalent to 
• Assuming [A], for every Boolean circuit of polynomial size
there is an equivalent ACC circuit of polynomial size
Binary encoding of a circuit C
24
Input x’
uib.no
Algorithms Research Group
Using the existence of small ACC circuits
• Recall our approach to faster Succinct 3SAT
• Under [A] there are poly-size ACC circuits equivalent to ’ and 
• A nondeterministic algorithm can
– Guess two small ACC circuits  and 
– Use them instead of ’ and 
• Have to ensure that branches with wrong guesses do not accidentally
output yes if the answer to Succinct 3SAT is no
– Wrongly guessing  is not a problem
• Then  does not satisfy the formula, we output no
– Wrongly guessing  is a problem
• If  encodes a different formula than C’, TT() might be satisfiable
even if TT(C) is not
• We might incorrectly answer yes
• After guessing we should verify that TT() = TT(’)
25
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
26
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
uib.no
Algorithms Research Group
Checking that C’ and  are equivalent
• We could make a circuit that tests whether it is possible to
satisfy ¬ [ C’(x) ⇔ (x) ]
• Run our Circuit SAT algorithm on it?
– It would not be an ACC circuit since it contains ’
• Solution:
– Guess a circuit that gives more information than C’
– Makes it easier to verify that it gives the right information
27
uib.no
Algorithms Research Group
The Circuit Gate Value Problem
• Input:
– Binary encoding  of ’-input circuit 
– Bitstring ’ ∈ {0,1}’
– Index  of a gate in 
• Question: Does gate  of  evaluate to 1 on input ’?
• Circuit Gate Value ∈ P
– Assuming [A] it has polynomial-size ACC circuits
28
uib.no
Algorithms Research Group
The Circuit Gate Value Problem
• By hardcoding a description of ’ into a Circuit Gate Value
Decider, we get a poly-size ACC circuit (’, ) such that:
– (’, ) = Value of gate  when ’ evaluates ’
• A guessed circuit (’, ) is correct if and only if:
May assume that the
– For all possible inputs ’, for all gate indices
 of ’:
•
•
•
•
fan-in of ′ is 2
If  is an AND-gate with inputs ,  then (’, ) = (’, ) ∧ (’, )
If  is an OR-gate with inputs ,  then (, ) = (, ) ∨ (, )
If  is a NOT-gate with inputs  then (, ) = ¬(, )
If  is the  th input gate then (, ) = []
• Can we set up an ACC circuit to test this?
29
uib.no
Algorithms Research Group
An ACC circuit to verify the behavior of a gate
• To verify correctness of an AND-gate  with inputs  and :
– (for all possible inputs ’)
30
uib.no
Algorithms Research Group
An ACC circuit to verify the behavior of a gate
• To verify correctness of an AND-gate  with inputs  and :
– (for all possible ’)
• Similar constructions for OR, NOT and INPUT gates
• To check consistency of all gates simultaneously, for one input ’:
– Build constant-depth checkers for each gate
– Feed them into an AND gate to get circuit ’
• -input circuit ’ has size poly(), so poly() gates
…
31
uib.no
Algorithms Research Group
An ACC circuit to verify the behavior of a gate
•  correctly simulates ’ if and only if ¬ is unsatisfiable
– Note: ¬ is an ACC circuit with  inputs and poly() size
– The ACC-Circuit-SAT algorithm runs in time


−
2
…
32
uib.no
Algorithms Research Group
-input Succinct 3SAT in NTIME[2
 −
]
• Assume: -input, poly()-size ACC-Circuit-SAT in time 2 −

• Input: string  encoding an -input circuit  of size poly()
– Construct circuit ′ such that ′()
is the ith clause
of TT
(C)

– Guess poly()-size ACC circuits  ⋅ and (⋅,⋅)
– Construct the ACC circuit ′(⋅) testing if  simulates ’
In some
branch,
) outputs the
If TT(C) is satisfiable,
thenon(’,
– Call the ACC-Circuit-SAT
algorithm
¬′
th
value
of the  gate of ’ on input ’
(⋅) encodes
a satisfying
• If ¬′ is satisfiable:
guess
for  is incorrect, output no
assignment
in of
≥ C’
1 branch
Else: E and
simulates
gates
so (′, OUT) = ′( ′ )
′ has • inputs
size poly(n)

– in
Compose
3 copies of  ⋅ with (⋅, OUT) to form D
Executes
2 − time
– Call the ACC-Circuit-SAT algorithm on ¬
– If ¬ is satisfiable: output no
» (W’ is not a satisfying assignment)
– Else: output yes (’ satisfies TT(C))
…
33
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
(ACC-Circuit-SAT in time


−
2
)
-input Succinct 3SAT in


−
NTIME[2
]
∧ (NEXP ⊆ ACC)
¬ (Non-det. time hierarchy theorem)
34
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
⇒
⇒
⇒⊥
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
II. Nontrivial ACC-Circuit-SAT algorithms exist
a. Decomposing ACC circuits using
multilinear polynomials
35
b. Quickly evaluating a multilinear
polynomial on many points
c. Reducing the number of variables
uib.no
Algorithms Research Group
Nontrivial algorithms for ACC Circuit SAT
• Three different routes
1. Coppersmith’s rectangular matrix multiplication algorithm
• (In the conference version)
2. Dynamic programming using the zeta transform
• (In the journal version)
3. Recursion
• (In the informal article)
• All exploit a structural decomposition of ACC developed in the 90’s
– [Yao’90, Beigel&Tarui’94, Allender&Gore’94]
36
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
II. Nontrivial ACC-Circuit-SAT algorithms exist
a. Decomposing ACC circuits using
multilinear polynomials
37
b. Quickly evaluating a multilinear
polynomial on many points
c. Reducing the number of variables
uib.no
Algorithms Research Group
Decomposing ACC circuits by polynomials
• Let  be an -input circuit of size , depth , with mod[m] gates
– Computation C(x1, … , xn) can be simulated by:
• Evaluating a “sparse” multilinear polynomial (1, … , )
• Looking up [(1, … , )] in a sparse 0-1 array A
The decomposition can be obtained algorithmically in () time
1 1 ACC
0 1Circuit
0 0 Satisfiability
0 1 1 0 to
1 checking
1 1 0 whether
0 1 0 there
1 1 0is
A=Reduces
some point  ∈ 0,1  with [()] = 1
 ,
 ≤ 2O(log
)
cells
 1 , … ,  = 811 5 7 + 242 4 5 + 51 6 8 + … + 31 2 3 4 5 6 7 8
≤ terms
38
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
II. Nontrivial ACC-Circuit-SAT algorithms exist
a. Decomposing ACC circuits using
multilinear polynomials
39
b. Quickly evaluating a multilinear
polynomial on many points
c. Reducing the number of variables
uib.no
Algorithms Research Group
Quickly evaluating a polynomial
• Why does a decomposition into polynomials help?
• A -term -variate multilinear polynomial  can be evaluated
– on all points of 0,1 
– in 2 ⋅   time
(assuming constant-time arithmetic)
• We spend poly() amortized time per point
– Even though  may be ≫ ()
– Compare to naïve 2 ⋅  ⋅   algorithm
40
uib.no
Algorithms Research Group
Quickly evaluating a polynomial
• Why does a decomposition into polynomials help?
• A -term -variate multilinear polynomial  can be evaluated
– on all points of 0,1 
– in 2 ⋅   time
(assuming constant-time arithmetic)
• Decompose  into multilinear 1, 2 as follows:
–  1 , 2 , … ,  = 1 ⋅ 1 2 , … ,  + 2 2 , … , 
• Then:
–  0, 2 , … ,  = 2 2 , … , 
–  1, 2 , … ,  = 1 2 , … ,  + 2 2 , … , 
• Gives a recursive algorithm
41
 
≤ 2 ⋅   + 2  − 1
≤ 2 ⋅ ()
uib.no
Algorithms Research Group
Exploiting fast evaluation of polynomials
• Idea to check satisfiability of an -input ACC circuit :
– Compute decomposition (1, … , ) = [(1, … , )]
– Evaluate  on all points x in 0,1 
– Check if some [()] = 1


−
2
()
• To get
time,  should have <  variables
– But C has  inputs!
42
uib.no
Algorithms Research Group
Outline of the proof
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
II. Nontrivial ACC-Circuit-SAT algorithms exist
a. Decomposing ACC circuits using
multilinear polynomials
43
b. Quickly evaluating a multilinear
polynomial on many points
c. Reducing the number of variables
uib.no
Algorithms Research Group
Reducing the number of variables
• Consider an -input circuit  for Circuit Satisfiability of size 
• Reduce the number of variables to  −  by a -blowup:
– Enumerate all assignments to 1 , 2 , … , 
– Hardcode each assignment into a new copy of 
– Take the OR of the resulting circuits
• Resulting circuit has size (2 ⋅ )
– Depth is increased by one
– Result is still an ACC circuit
– Satisfiable if and only if C is satisfiable!
44
uib.no
Algorithms Research Group
Running for
time:
A faster algorithm
ACC
Circuit
SAT
 ,
 2O(log
′)
≤
• Testing satisfiability of circuit

,
O(log
2 )

2
≤
–  variables, size , depth , with mod[] gates

 , 2 +log , )
O(log
2
• Pick  = 
– ( depends onO(k
,)
 , +time:
 , )
Running
log
 2
(2⋅−
)
1. Compute the -blowup
’
of  
,

,
O(n
+ log
)



2
– Size 2 ⋅  and(2
depth
 +())
1
−
≤
≤
≤
′

–

′
≤ 2 −
≤2
2. Compute a decomposition of ’
– Sparse lookup table  of a sparse multilinear polynomial 
3. Evaluate () for all  ∈ 0,1
−
4. Output yes if and only if [()] for some  ∈ 0,1
45
−
uib.no
Algorithms Research Group
What happened?
• Where did the speed-up come from?
• The algorithm to evaluate the polynomial beats brute force
when the number of terms is large compared to 
• By blowing up the circuit, we increased the size of the circuit
– And therefore the number of terms in the polynomial
• This allows the ACC Circuit SAT algorithm to beat brute force
46
uib.no
Algorithms Research Group
QED
I. Nontrivial ACC-Circuit-SAT algorithms imply NEXP ⊄ ACC
a. NEXP-completeness
of Succinct 3SAT
b. Small witness circuits
for Succinct 3SAT
c. Checking an
assignment by
analyzing a circuit
d. ACC circuits simulate
Boolean circuits
e. Verifying a guessed
circuit
II. Nontrivial ACC-Circuit-SAT algorithms exist
a. Decomposing ACC circuits using
multilinear polynomials
b. Quickly evaluating a multilinear
polynomial on many points
c. Reducing the number of variables
NEXP ⊄ ACC
47
uib.no
Algorithms Research Group
Conclusion
• An algorithm for Circuit Satisfiability that is slightly faster than
brute force can be turned into a circuit complexity lower bound
• In 2011 this led to a proof that NEXP ⊄ ACC
• Follow-up work proves size lower bounds for more general circuits
– [STOC’14]: ACC with threshold gates at the bottom layer
• There are many other transference theorems on how algorithmic
advances imply circuit lower bounds [Oliveira’13]
– Derandomization
– Learning algorithms
– Compression algorithms
• Plenty of algorithmic challenges in circuit complexity!
48
uib.no
Algorithms Research Group

similar documents