Documentation

Complexity.Computability.Circuit.Frontier.Reduction

From small circuits to wide graphs #

This file combines the three ingredients of the frontier method for a single input length:

Frontier demand (Network.logb_ncard_accepted_le). If the accepted set of a network is K-rectangle-free and has at least q K ^ 2 elements, where q = |U|, then every layout of width w satisfies log_q |accepted| ≤ w + d + m + 3 log_q K + log_q (|V| + 1) for degrees at most d and at most m inputs read per vertex. The unread inputs cost nothing: by the support lemma they carry fewer than K assignments. No uniqueness of satisfying assignments is needed.

The reduction theorem (exists_graph_of_decides). Let c be a circuit with s inner gates (gates of positive arity; constants are free) of fan-in at most r ≥ 2, over any basis on a finite alphabet U with q ≥ 2 symbols, that decides a K-rectangle-free set S ⊆ U^n with |S| ≥ q K ^ 2. Then there is a connected, loopless multigraph G of maximum degree r + 1 with at most 2 r s + 3 vertices and cycle rank

β₁(G) ≤ (r - 1) s - n + log_q K + 1,

every layout of which has width at least

log_q |S| - 3 log_q K - log_q (|V(G)| + 1) - (r + 2).

The graph is that of the circuit (Compiler.graph). The bound on the cycle rank is the count of the compiler, together with the support lemma, which says that the circuit reads all but log_q K of its inputs. The bound on the width is frontier demand for the constraint network of the circuit, which accepts exactly S.

For a dense set log_q |S| ≈ n, so a small circuit gives a graph whose cycle rank is about (r - 1) s - n but all of whose layouts have width about n.

Main definitions #

Main results #

source
def Cslib.Circuits.Circuit.Decides {σ : Signature} {U : Type u_1} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ U) (Acc : Set U) (S : Set (Fin n → U)) :
Prop

A circuit with one output decides a set of inputs S, accepting the values in Acc, when an input lies in S exactly if the output of the circuit lies in Acc.

Instances For
    source
    theorem Cslib.Circuits.Circuit.Computes.decides {σ : Signature} {U : Type u_1} {n : ℕ} {c : Circuit σ n 1} {I : Interpretation σ U} {f : (Fin n → U) → U} (h : c.Computes I (single f)) (Acc : Set U) :
    c.Decides I Acc {x : Fin n → U | f x ∈ Acc}

    A circuit computing a function f decides the set of inputs that f maps into Acc; for a Boolean function, with Acc = {true}, the set of inputs it maps to true.

    Frontier demand for networks #

    source
    theorem Cslib.Circuits.Frontier.Network.ncard_accepted_le_pow {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} [Finite ι] [Finite U] [Finite E] (N : Network U ι V E) {K : ℕ} [Nonempty U] (hfree : RectangleFree N.accepted K) (hbig : Nat.card U * K ^ 2 ≤ N.accepted.ncard) (π : Layout V) {w d m : ℕ} (hw : N.width π ≤ w) (hd : N.MaxDegreeLE d) (hm : ∀ (v : V), (N.readAt v).ncard ≤ m) :
    N.accepted.ncard ≤ K ^ 3 * (Nat.card V + 1) * Nat.card U ^ (w + d + m)

    Frontier demand, counted. If the accepted set of a network is K-rectangle-free with at least |U| K ^ 2 elements, then a layout of width at most w, in a network of degree at most d reading at most m inputs per vertex, bounds it by |accepted| ≤ K ^ 3 (|V| + 1) |U| ^ (w + d + m). The unread inputs are paid for by the support lemma.

    source
    theorem Cslib.Circuits.Frontier.Network.logb_ncard_accepted_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} [Finite ι] [Finite U] [Finite E] (N : Network U ι V E) {K : ℕ} [Nontrivial U] (hfree : RectangleFree N.accepted K) (hbig : Nat.card U * K ^ 2 ≤ N.accepted.ncard) (π : Layout V) {w d m : ℕ} (hw : N.width π ≤ w) (hd : N.MaxDegreeLE d) (hm : ∀ (v : V), (N.readAt v).ncard ≤ m) :
    Real.logb ↑(Nat.card U) ↑N.accepted.ncard ≤ ↑w + ↑d + ↑m + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)

    Frontier demand. If the accepted set of a network is K-rectangle-free with at least q K ^ 2 elements, where q = |U| ≥ 2, then a layout of width at most w, in a network of degree at most d reading at most m inputs per vertex, satisfies

    log_q |accepted| ≤ w + d + m + 3 log_q K + log_q (|V| + 1).

    No uniqueness of satisfying assignments is needed.

    Circuits deciding rectangle-free sets #

    source
    theorem Cslib.Circuits.Frontier.accepted_network_of_decides {σ : Signature} {U : Type u_1} {n : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ n 1} {S : Set (Fin n → U)} (hS : c.Decides I Acc S) :
    (Compiler.network c I fun (x : Fin 1) => Acc).accepted = S

    The constraint network of a circuit deciding S accepts exactly S.

    source
    theorem Cslib.Circuits.Frontier.pow_ncard_compl_read_lt {σ : Signature} {U : Type u_1} {n : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ n 1} {S : Set (Fin n → U)} {K : ℕ} [Finite U] [Nontrivial U] (hS : c.Decides I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) :
    Nat.card U ^ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ.ncard < K

    The support lemma for circuits. A circuit deciding a large rectangle-free set reads all but fewer than log_q K of its inputs.

    source
    theorem Cslib.Circuits.Frontier.cycleRank_le {σ : Signature} {U : Type u_1} {n : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ n 1} {K r : ℕ} [Finite U] [Nontrivial U] (hfan : c.FanInAtMost r) (hunread : Nat.card U ^ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ.ncard < K) :
    ↑(Compiler.graph c).cycleRank ≤ (↑r - 1) * ↑c.innerSize - ↑n + Real.logb ↑(Nat.card U) ↑K + 1

    The cycle rank of the graph of a circuit is at most (r - 1) s - n + log_q K + 1 for fan-in at most r, where s counts the inner gates, when the inputs the circuit does not read carry fewer than K assignments. By the support lemma this is so for a circuit deciding a large K-rectangle-free set (pow_ncard_compl_read_lt).

    source
    theorem Cslib.Circuits.Frontier.logb_ncard_le_width {σ : Signature} {U : Type u_1} {n : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ n 1} {S : Set (Fin n → U)} {K r : ℕ} [Finite U] [Nontrivial U] (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : c.Decides I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) (π : Layout (Compiler.Vertex c)) :
    Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑((Compiler.graph c).width π) + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card (Compiler.Vertex c)) + 1)

    Every layout of the graph of a circuit is wide. For a circuit of fan-in at most r ≥ 2 deciding a large K-rectangle-free set S, every layout π of its graph satisfies log_q |S| ≤ width π + (r + 2) + 3 log_q K + log_q (|V| + 1).

    source
    theorem Cslib.Circuits.Frontier.exists_graph_of_decides {σ : Signature} {U : Type u_1} {n : ℕ} {I : Interpretation σ U} {Acc : Set U} {c : Circuit σ n 1} {S : Set (Fin n → U)} {K r : ℕ} [Finite U] [Nontrivial U] (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hS : c.Decides I Acc S) (hfree : RectangleFree S K) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) :
    ∃ (V : Type) (E : Type) (_ : Finite V) (x : Finite E) (G : Multigraph V E), G.toSimpleGraph.Connected ∧ G.Loopless ∧ G.MaxDegreeLE (r + 1) ∧ Nat.card V ≤ 2 * r * c.innerSize + 3 ∧ ↑G.cycleRank ≤ (↑r - 1) * ↑c.innerSize - ↑n + Real.logb ↑(Nat.card U) ↑K + 1 ∧ ∀ (π : Layout V), Real.logb ↑(Nat.card U) ↑S.ncard ≤ ↑(G.width π) + (↑r + 2) + 3 * Real.logb ↑(Nat.card U) ↑K + Real.logb (↑(Nat.card U)) (↑(Nat.card V) + 1)

    The reduction theorem. A circuit with s inner gates of fan-in at most r ≥ 2, over any basis on U, deciding a K-rectangle-free set S ⊆ U^n with |S| ≥ q K ^ 2, where q = |U| ≥ 2, yields a connected, loopless multigraph of maximum degree r + 1 with at most 2 r s + 3 vertices and cycle rank at most (r - 1) s - n + log_q K + 1, every layout of which has width at least log_q |S| - 3 log_q K - log_q (|V| + 1) - (r + 2).