Exact-multiplicity CSP and CNF compilation of circuits via the frontier compiler

Compiles a circuit c : Circuit σ n m over an arbitrary Boolean signature σ into a Boolean constraint satisfaction instance Compiler.toCSP c : CSP (CircuitRel σ m) ℕ on its reachable wires (Compiler.Signal c), and from there via Cslib.Logic.PL.CSP.toCNF into a CNF formula Compiler.toCNF c I acc accompanied by an explicit unread-input / unconstrained-wire shift Compiler.freeShift c I acc, such that:

1. Bounded scope and clause width: when c.FanInAtMost k, every constraint of toCSP c (and therefore every clause of toCNF c I acc) has width at most k + 1.
2. Gate-size variable bound: (toCNF c I acc).numVars ≤ k * c.size + m (independent of the ambient input count n), bounded through Compiler.card_signal_le on Compiler.Signal c.
3. Exact multiplicity (acceptCount_eq_two_pow_freeShift_mul_modelCount): c.acceptCount I acc = 2 ^ freeShift c I acc * (toCNF c I acc).modelCount, proved through the frontier constraint network Compiler.network c I _, its exactness and trace-uniqueness theorems (Compiler.satisfies_iff, Compiler.eq_trace, Compiler.accepted_network), and read-dependence (Network.dependsOn_read).

Source relation and library extensions

Appendix C.1 of [OAI26c] (p. 51) introduces one variable per gate (n + s variables total) for single-output De Morgan (AND/OR/NOT) circuits to preserve satisfiability in 3-CNF. Generalizing to arbitrary signatures σ and multi-output acceptance predicates acc, pruning to reachable wires (Signal c) so the variable bound k * c.size + m depends on gate count rather than ambient input count n, and tracking exact multiplicity via 2 ^ freeShift for #Circuit-SAT are original extensions built on Cslib.Circuits.Frontier.Compiler and Cslib.Logic.PL.CSP.ToCNF.

Main definitions

• Cslib.Circuits.Frontier.Compiler.satisfiedPairsEquiv: bijection between input/edge-assignment pairs satisfying Compiler.network and Network.accepted.
• Cslib.Circuits.Frontier.Compiler.CircuitRel, Cslib.Circuits.Frontier.Compiler.circuitSem: relation alphabet σ.Op ⊕ Fin m and Boolean semantics for gate evaluation and output acceptance.
• Cslib.Circuits.Frontier.Compiler.toCSP, Cslib.Circuits.Frontier.Compiler.toCNF, Cslib.Circuits.Frontier.Compiler.freeShift, Cslib.Circuits.Frontier.Compiler.toSatCNF, Cslib.Circuits.Frontier.Compiler.satFreeShift: reachable-wire CSP and exact-multiplicity CNF compilation.

Main results

• Cslib.Circuits.Frontier.Compiler.length_scope_le_of_mem_toCSP, Cslib.Circuits.Frontier.Compiler.length_le_of_mem_toCNF: constraint scopes and clauses have length at most k + 1 when c.FanInAtMost k.
• Cslib.Circuits.Frontier.Compiler.numVars_toCNF_le: (toCNF c I acc).numVars ≤ k * c.size + m.
• Cslib.Circuits.Frontier.Compiler.acceptCount_eq_two_pow_freeShift_mul_modelCount, Cslib.Circuits.Frontier.Compiler.satCount_eq_two_pow_satFreeShift_mul_modelCount: exact counting identities reducing #Circuit-SAT to bounded-width #SAT.
• Cslib.Circuits.Frontier.Compiler.satisfiable_toSatCNF_iff: satisfiability equivalence.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix C.1, p. 51.
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

Uniqueness bijection on Compiler.network

noncomputable def Cslib.Circuits.Frontier.Compiler.satisfiedPairsEquiv {σ : Signature} {n m : ℕ} {U : Type u_1} (c : Circuit σ n m) (I : Interpretation σ U) (Acc : Fin m → Set U) : { p : (Fin n → U) × (Edge c → U) // (network c I Acc).Satisfies p.1 p.2 } ≃ ↑(network c I Acc).accepted

By Compiler.satisfies_iff and Compiler.eq_trace, pairs (x, α) satisfying Compiler.network c I Acc correspond bijectively to accepted inputs x ∈ (network c I Acc).accepted with zero multiplicity inflation.

Constructive CSP and CNF compilation along reachable wires

@[reducible, inline]

abbrev Cslib.Circuits.Frontier.Compiler.CircuitRel (σ : Signature) (m : ℕ) : Type

Relation alphabet for frontier CSP compilation of an m-output circuit over σ:

• .inl op: a gate-evaluation relation on outWire :: argWires;
• .inr o: the unary acceptance predicate at output o : Fin m.

def Cslib.Circuits.Frontier.Compiler.circuitSem {σ : Signature} {m : ℕ} (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : CircuitRel σ m → List Bool → Bool

Boolean relation semantics for CircuitRel σ m:

• .inl op accepts outBit :: inBits iff inBits.length = σ.Arity op and outBit = I op (fun a => inBits.getD a.val false);
• .inr o accepts [b] iff acc o b = true.

def Cslib.Circuits.Frontier.Compiler.reachStep {σ : Signature} (n : ℕ) (seen : List ℕ) (gj : (σ.Op × List ℕ) × ℕ) : List ℕ

One backward reachability step on a gate (g, j): if gate wire n + j is already marked reachable, prepend its argument wires g.2.

def Cslib.Circuits.Frontier.Compiler.reachWiresCode {σ : Signature} (n : ℕ) (code : List (σ.Op × List ℕ) × List ℕ) : List ℕ

Backward pass computing the list of reachable wire numbers from a serialized circuit (gates, outputs) on n inputs.

def Cslib.Circuits.Frontier.Compiler.reachGateCountCode {σ : Signature} (n : ℕ) (code : List (σ.Op × List ℕ) × List ℕ) : ℕ

Number of reachable internal gates in a serialized circuit on n inputs.

def Cslib.Circuits.Frontier.Compiler.toCSPCode {σ : Signature} (m n : ℕ) (code : List (σ.Op × List ℕ) × List ℕ) : Logic.PL.CSP (CircuitRel σ m) ℕ

Serialized circuit-to-CSP compiler emitting one gate constraint (Sum.inl g.1, (n + j) :: g.2) for each reachable gate (g, j) followed by one unary output constraint (Sum.inr o, [code.2.getD o.val 0]) for each o : Fin m.

def Cslib.Circuits.Frontier.Compiler.toCSP {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Logic.PL.CSP (CircuitRel σ m) ℕ

Reachable-wire Boolean CSP compiled from c : Circuit σ n m.

def Cslib.Circuits.Frontier.Compiler.toCNFCode {σ : Signature} (I : Interpretation σ Bool) {m : ℕ} (acc : Fin m → Bool → Bool) (n : ℕ) (code : List (σ.Op × List ℕ) × List ℕ) : Logic.PL.CNF ℕ

Serialized circuit-to-CNF compiler obtained by applying CSP.toCNF (circuitSem I acc) to toCSPCode m n code.

def Cslib.Circuits.Frontier.Compiler.freeShiftCode {σ : Signature} (I : Interpretation σ Bool) {m : ℕ} (acc : Fin m → Bool → Bool) (n : ℕ) (code : List (σ.Op × List ℕ) × List ℕ) : ℕ

Exact binary-exponent shift accounting for unread inputs and reachable wires that do not appear syntactically in toCNFCode (e.g. unconstrained outputs).

def Cslib.Circuits.Frontier.Compiler.toCNF {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : Logic.PL.CNF ℕ

Exact-multiplicity CNF formula compiled from c : Circuit σ n m along its reachable wires.

def Cslib.Circuits.Frontier.Compiler.freeShift {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : ℕ

Unread-input / unconstrained-wire exponent shift accompanying toCNF c I acc.

def Cslib.Circuits.Frontier.Compiler.toSatCNF {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : Logic.PL.CNF ℕ

Specialization of toCNF to 1-output #Circuit-SAT (accepting true at output 0).

def Cslib.Circuits.Frontier.Compiler.satFreeShift {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : ℕ

Specialization of freeShift to 1-output #Circuit-SAT.

Local constraint semantics

Equivalence of reachWiresCode and Compiler.Reach

Structural bounds on toCSP and toCNF

theorem Cslib.Circuits.Frontier.Compiler.length_scope_le_of_mem_toCSP {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {k : ℕ} (hfan : c.FanInAtMost k) {con : Logic.PL.Constraint (CircuitRel σ m) ℕ} (hcon : con ∈ toCSP c) : con.2.length ≤ k + 1

Every constraint in toCSP c has scope length at most k + 1 when c.FanInAtMost k.

theorem Cslib.Circuits.Frontier.Compiler.length_le_of_mem_toCNF {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) {k : ℕ} (hfan : c.FanInAtMost k) {cl : Logic.PL.Clause ℕ} (hcl : cl ∈ toCNF c I acc) : List.length cl ≤ k + 1

Every clause of toCNF c I acc has length at most k + 1 when c.FanInAtMost k.

theorem Cslib.Circuits.Frontier.Compiler.vars_toCSP_subset {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : (toCSP c).vars.toFinset ⊆ (reachWiresCode n c.code).toFinset

Every variable occurring in toCSP c belongs to (reachWiresCode n c.code).toFinset.

theorem Cslib.Circuits.Frontier.Compiler.vars_toCNF_subset {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : (toCNF c I acc).vars.toFinset ⊆ (reachWiresCode n c.code).toFinset

Every variable occurring in toCNF c I acc belongs to (reachWiresCode n c.code).toFinset.

theorem Cslib.Circuits.Frontier.Compiler.card_reachWiresCode_toFinset {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : (reachWiresCode n c.code).toFinset.card = Nat.card (Signal c)

(reachWiresCode n c.code).toFinset has cardinality Nat.card (Signal c).

theorem Cslib.Circuits.Frontier.Compiler.numVars_toCNF_le {σ : Signature} {n m : ℕ} {c : Circuit σ n m} (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) {k : ℕ} (hfan : c.FanInAtMost k) : (toCNF c I acc).numVars ≤ k * c.size + m

When c.FanInAtMost k, toCNF c I acc uses at most k * c.size + m distinct variables.

theorem Cslib.Circuits.Frontier.Compiler.numVars_toCNF_le_add_size {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : (toCNF c I acc).numVars ≤ n + c.size

toCNF c I acc uses at most n + c.size distinct variables (all wire numbers lie below n + c.size).

Exact counting through Compiler.network

theorem Cslib.Circuits.Frontier.Compiler.acceptCount_eq_two_pow_freeShift_mul_modelCount {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : c.acceptCount I acc = 2 ^ freeShift c I acc * (toCNF c I acc).modelCount

Exact counting via Compiler.network. For every circuit c : Circuit σ n m, interpretation I, and output predicate acc, the number of accepted inputs equals 2 ^ freeShift c I acc * (toCNF c I acc).modelCount.

theorem Cslib.Circuits.Frontier.Compiler.satCount_eq_two_pow_satFreeShift_mul_modelCount {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : c.satCount I = 2 ^ satFreeShift c I * (toSatCNF c I).modelCount

Single-output #Circuit-SAT specialization of acceptCount_eq_two_pow_freeShift_mul_modelCount.

theorem Cslib.Circuits.Frontier.Compiler.satisfiable_toCNF_iff {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : (toCNF c I acc).Satisfiable ↔ ∃ (x : Fin n → Bool), ∀ (o : Fin m), acc o (c.eval I x o) = true

toCNF c I acc is satisfiable iff c has an input accepted by acc.

theorem Cslib.Circuits.Frontier.Compiler.satisfiable_toSatCNF_iff {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : (toSatCNF c I).Satisfiable ↔ ⟨n, c⟩ ∈ Complexity.SignatureCircuitSAT I

toSatCNF c I is satisfiable iff ⟨n, c⟩ ∈ SignatureCircuitSAT I.