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