Arithmetization of Boolean formulas

The mathematical part of the paper's lem:formula-arithmetization: replace conjunction by multiplication, disjunction by 1 - (1 - f) * (1 - g), and negation by 1 - f. Each variable's degree is bounded by its occurrence count. The evaluator and its cost in an effective finite-field representation are separate.

def MIPRE.SAT.Fml.arith {F : Type u_1} {σ : Type u_2} [CommRing F] (ρ : ℕ → σ) : Fml → MvPolynomial σ F

Arithmetize after assigning a polynomial variable to every input index.

Equations

• MIPRE.SAT.Fml.arith ρ (MIPRE.SAT.Fml.inp i) = MvPolynomial.X (ρ i)
• MIPRE.SAT.Fml.arith ρ (MIPRE.SAT.Fml.const b) = MvPolynomial.C (MIPRE.LowDegree.ofBool b)
• MIPRE.SAT.Fml.arith ρ (f.and g) = MIPRE.SAT.Fml.arith ρ f * MIPRE.SAT.Fml.arith ρ g
• MIPRE.SAT.Fml.arith ρ (f.or g) = 1 - (1 - MIPRE.SAT.Fml.arith ρ f) * (1 - MIPRE.SAT.Fml.arith ρ g)
• MIPRE.SAT.Fml.arith ρ f.not = 1 - MIPRE.SAT.Fml.arith ρ f

def MIPRE.SAT.Fml.occurrences {σ : Type u_2} [DecidableEq σ] (ρ : ℕ → σ) (j : σ) : Fml → ℕ

The occurrence count, including collisions in the variable assignment ρ.

Equations

• MIPRE.SAT.Fml.occurrences ρ j (MIPRE.SAT.Fml.inp i) = if j = ρ i then 1 else 0
• MIPRE.SAT.Fml.occurrences ρ j (MIPRE.SAT.Fml.const b) = 0
• MIPRE.SAT.Fml.occurrences ρ j (f.and g) = MIPRE.SAT.Fml.occurrences ρ j f + MIPRE.SAT.Fml.occurrences ρ j g
• MIPRE.SAT.Fml.occurrences ρ j (f.or g) = MIPRE.SAT.Fml.occurrences ρ j f + MIPRE.SAT.Fml.occurrences ρ j g
• MIPRE.SAT.Fml.occurrences ρ j f.not = MIPRE.SAT.Fml.occurrences ρ j f

theorem MIPRE.SAT.Fml.eval_arith {F : Type u_1} {σ : Type u_2} [CommRing F] (ρ : ℕ → σ) (f : Fml) (x : σ → Bool) : (MvPolynomial.eval fun (j : σ) => LowDegree.ofBool (x j)) (arith ρ f) = LowDegree.ofBool (eval (fun (i : ℕ) => x (ρ i)) f)

On Boolean inputs, arithmetization agrees with the original formula.

theorem MIPRE.SAT.Fml.degreeOf_arith_le {F : Type u_1} {σ : Type u_2} [CommRing F] [DecidableEq σ] [Nontrivial F] (ρ : ℕ → σ) (f : Fml) (j : σ) : MvPolynomial.degreeOf j (arith ρ f) ≤ occurrences ρ j f

The degree in each variable is at most its number of syntactic occurrences.