The circuit-to-3SAT reduction

Circuit.tseitin C inp gv is the 3SAT formula of a circuit C on variables inp i for its inputs and gv g for its gates (lem:circuit-to-sat-reduction, lem:tseitin with the output-wire conjunct of the F7.2 erratum): for every gate the clauses saying that its variable is the gate's function of its arguments' variables, and the unit clause on the output gate. tseitin_values: a satisfying assignment carries the gate values. The tableau of the Cook–Levin theorem is this reduction applied to the local check circuit at every window (planning/succinct-cook-levin.md, S1).

def MIPRE.SAT.cl {V : Type u_1} (a b c : Lit V) : Clause3 V

A clause from three literals.

Equations

• MIPRE.SAT.cl a b c = { l₁ := a, l₂ := b, l₃ := c }

def MIPRE.SAT.gateClauses {V : Type u_1} (inp gv : ℕ → V) (y : V) : Gate → List (Clause3 V)

The consistency clauses of a gate whose variable is y, over the input variables inp and the gate variables gv.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.SAT.gateClauses inp gv y (MIPRE.SAT.Gate.const b) = [MIPRE.SAT.cl { var := y, pos := b } { var := y, pos := b } { var := y, pos := b }]

theorem MIPRE.SAT.gateClauses_iff {V : Type u_1} (inp gv : ℕ → V) (y : V) (g : Gate) (w : V → Bool) (vals : List Bool) (hv : ∀ u ∈ g.refs, vals.getD u false = w (gv u)) : (∀ c ∈ gateClauses inp gv y g, Clause3.eval w c = true) ↔ w y = Gate.eval (fun (i : ℕ) => w (inp i)) vals g

The clauses of a gate hold iff its variable carries the gate's value, when the argument variables carry the argument values.

def MIPRE.SAT.Circuit.tseitin {V : Type u_1} (C : Circuit) (inp gv : ℕ → V) : Cnf3 V

The circuit-to-3SAT formula of C: the consistency clauses of every gate, and the unit clause on the output gate.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.SAT.Circuit.RefsLt (C : Circuit) : Prop

Every gate reads only earlier gates.

Equations

• C.RefsLt = ∀ (k : ℕ) (h : k < C.gates.length), ∀ u ∈ C.gates[k].refs, u < k

theorem MIPRE.SAT.Circuit.WellFormed.refsLt {C : Circuit} (h : C.WellFormed) : C.RefsLt

theorem MIPRE.SAT.Circuit.tseitin_values {V : Type u_1} (C : Circuit) (hC : C.RefsLt) (inp gv : ℕ → V) (w : V → Bool) (hSat : ∀ c ∈ C.tseitin inp gv, Clause3.eval w c = true) (g : ℕ) : g < C.gates.length → w (gv g) = C.valueAt (fun (i : ℕ) => w (inp i)) g

A satisfying assignment of the gate clauses carries the gate values.

def MIPRE.SAT.Circuit.InputsLt (C : Circuit) : Prop

Every input gate reads an existing input.

Equations

• C.InputsLt = ∀ (i : ℕ), MIPRE.SAT.Gate.input i ∈ C.gates → i < C.inputs

theorem MIPRE.SAT.Circuit.WellFormed.inputsLt {C : Circuit} (h : C.WellFormed) : C.InputsLt

theorem MIPRE.SAT.Circuit.valueAt_congr (C : Circuit) (hin : C.InputsLt) (x x' : ℕ → Bool) (hx : ∀ i < C.inputs, x i = x' i) (g : ℕ) : C.valueAt x g = C.valueAt x' g

The gate values depend only on the inputs the circuit reads.

theorem MIPRE.SAT.Circuit.eval_congr (C : Circuit) (hin : C.InputsLt) (x x' : ℕ → Bool) (hx : ∀ i < C.inputs, x i = x' i) : C.eval x = C.eval x'

theorem MIPRE.SAT.Circuit.eval_of_tseitin_sat {V : Type u_1} (C : Circuit) (hC : C.RefsLt) (hin : C.InputsLt) (hne : C.gates ≠ []) (inp gv : ℕ → V) (x : ℕ → Bool) (w : V → Bool) (hx : ∀ i < C.inputs, w (inp i) = x i) (hSat : (C.tseitin inp gv).Sat w) : C.eval x = true

Soundness: a satisfying assignment of the formula agreeing with x on the inputs witnesses C(x) = 1.

theorem MIPRE.SAT.Circuit.tseitin_sat_of_values {V : Type u_1} (C : Circuit) (hC : C.RefsLt) (inp gv : ℕ → V) (w : V → Bool) (hwg : ∀ g < C.gates.length, w (gv g) = C.valueAt (fun (i : ℕ) => w (inp i)) g) (hx : (C.eval fun (i : ℕ) => w (inp i)) = true) : (C.tseitin inp gv).Sat w

Completeness, for a given assignment: one that carries the gate values on the gate variables satisfies the formula when the circuit accepts the bits it reads on the inputs.