The reduction emitter: clause and CNF machines

Machinery for emitting encoded CNF formulas whose variables are mixed-radix numerals (Tableau.flatVar): literal descriptors name a sign, a top digit, and four digit sources (registers or constants); emitClauseTM emits one clause from a descriptor list; emitCNFTM folds clause emitters over a formula. Each machine's Hoare specification appends exactly the CNF.encode-image of the denoted formula to the output accumulator.

The family drivers (one per tableauCNFFlat clause family) instantiate these with the concrete descriptor lists mirroring each family's definition.

def Complexity.SAT.Lit.word (ℓ : Lit) : List Bool

The encoded word of one literal inside a clause (Clause.encode_cons').

Equations

• ℓ.word = [ℓ.sign, ℓ.sign] ++ List.replicate (2 * ℓ.var) true ++ [false, true]

theorem Complexity.SAT.Clause.encode_cons_word (ℓ : Lit) (ℓs : Clause) : encode (ℓ :: ℓs) = ℓ.word ++ ℓs.encode

Prepending a literal to a clause prepends its encoded word (Lit.word) to the clause encoding.

theorem Complexity.SAT.Clause.encode_map {α : Type u_1} (g : α → Lit) (l : List α) : encode (List.map g l) = List.flatMap (fun (a : α) => (g a).word) l

A mapped clause encodes as the concatenation of its literal words.

theorem Complexity.SAT.CNF.encode_map {α : Type u_1} (g : α → Clause) (l : List α) : encode (List.map g l) = List.flatMap (fun (a : α) => (g a).encode ++ [true, false]) l

A mapped CNF encodes as the concatenation of its clause words.

structure Complexity.SAT.LitDesc (n : ℕ) : Type

Literal descriptor: the machine-level recipe for one literal — a sign, the hardwired top digit, and the four mixed-radix digit sources.

• sign : Bool

  The literal's sign: true for a positive literal, false for negated.

• tag : ℕ

  The hardwired top (most significant) mixed-radix digit of the variable.

• sa : TM.DigitSrc n

  Source of the first mixed-radix digit below the tag (radix A).

• sb : TM.DigitSrc n

  Source of the second mixed-radix digit below the tag (radix B).

• sc : TM.DigitSrc n

  Source of the third mixed-radix digit below the tag (radix C).

• sd : TM.DigitSrc n

  Source of the fourth (least significant) mixed-radix digit (radix D).

def Complexity.SAT.LitDesc.tm {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (desc : LitDesc n) : TM n

The emitting machine of one descriptor.

Equations

• Complexity.SAT.LitDesc.tm rA rB rC rD tmp tmp2 desc = Complexity.TM.emitVarLitTM rA rB rC rD tmp tmp2 desc.sign desc.tag desc.sa desc.sb desc.sc desc.sd

def Complexity.SAT.LitDesc.Spec {n : ℕ} (work₀ : Fin n → Tape) (tmp tmp2 : Fin n) (M A B C D : ℕ) (desc : LitDesc n) (ℓ : Lit) : Prop

Descriptor denotation: desc denotes the literal ℓ over the work tapes work₀ with radices A B C D, all intermediate numeral values capped by M.

Equations

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

theorem Complexity.SAT.LitDesc.Spec.var_le {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} {M A B C D : ℕ} {desc : LitDesc n} {ℓ : Lit} (h : Spec work₀ tmp tmp2 M A B C D desc ℓ) : ℓ.var ≤ M

Denoted variables are capped.

theorem Complexity.SAT.LitDesc.Spec.emit {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) {M A B C D : ℕ} (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) {desc : LitDesc n} {ℓ : Lit} {work₀ : Fin n → Tape} (hspec : Spec work₀ tmp tmp2 M A B C D desc ℓ) (z : ℕ) (hz : z ≤ M) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin n), TM.Parked (work₀ i)) (hrA : work₀ rA = TM.regTape A) (hrB : work₀ rB = TM.regTape B) (hrC : work₀ rC = TM.regTape C) (hrD : work₀ rD = TM.regTape D) : (tm rA rB rC rD tmp tmp2 desc).HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 z) ys) (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 ℓ.var) (ys ++ ℓ.word)) (TM.emitVarBudget M)

Per-descriptor emission. A denoting descriptor's machine appends the literal's encoded word, moving the scratches to the literal's variable.

theorem Complexity.SAT.emitLits_hoareTime {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) {M A B C D : ℕ} (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) (inp₀ : Tape) (hinp₀ : TM.Parked inp₀) {descs : List (LitDesc n)} {cl : Clause} {work₀ : Fin n → Tape} : List.Forall₂ (LitDesc.Spec work₀ tmp tmp2 M A B C D) descs cl → ∀ z ≤ M, ∀ (ys : List Bool), (∀ (i : Fin n), TM.Parked (work₀ i)) → work₀ rA = TM.regTape A → work₀ rB = TM.regTape B → work₀ rC = TM.regTape C → work₀ rD = TM.regTape D → (TM.bigSeqTM (List.map (LitDesc.tm rA rB rC rD tmp tmp2) descs)).HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 z) ys) (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 (List.foldl (fun (x : ℕ) (ℓ : Lit) => ℓ.var) z cl)) (ys ++ cl.encode)) (descs.length * (TM.emitVarBudget M + 1) + 1)

Chained literal emission. A descriptor list denoting the clause cl appends Clause.encode cl, scratches ending at the last variable (or staying at z for the empty clause).

theorem Complexity.SAT.foldl_var_le {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} {M A B C D : ℕ} {descs : List (LitDesc n)} {cl : Clause} : List.Forall₂ (LitDesc.Spec work₀ tmp tmp2 M A B C D) descs cl → ∀ z ≤ M, List.foldl (fun (x : ℕ) (ℓ : Lit) => ℓ.var) z cl ≤ M

Denoted clause variables are capped, hence so is the scratch fold.

def Complexity.SAT.emitClauseTM {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (descs : List (LitDesc n)) : TM n

Emit one clause: the literals, the clause separator [1,0], and a scratch reset (so clause emitters compose at the scratch-0 state).

Equations

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

def Complexity.SAT.clauseBudget (L M : ℕ) : ℕ

Time budget of a clause emitter with at most L literals.

Equations

• Complexity.SAT.clauseBudget L M = L * (Complexity.TM.emitVarBudget M + 1) + 2 * Complexity.TM.opBudget M + 6

theorem Complexity.SAT.emitClauseTM_hoareTime {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) {M A B C D : ℕ} (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) {descs : List (LitDesc n)} {cl : Clause} {work₀ : Fin n → Tape} (hf : List.Forall₂ (LitDesc.Spec work₀ tmp tmp2 M A B C D) descs cl) {L : ℕ} (hL : descs.length ≤ L) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin n), TM.Parked (work₀ i)) (hrA : work₀ rA = TM.regTape A) (hrB : work₀ rB = TM.regTape B) (hrC : work₀ rC = TM.regTape C) (hrD : work₀ rD = TM.regTape D) : (emitClauseTM rA rB rC rD tmp tmp2 descs).HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 0) (ys ++ (cl.encode ++ [true, false]))) (clauseBudget L M)

emitClauseTM Hoare specification: appends Clause.encode cl ++ [true, false], scratches 0 to 0.

def Complexity.SAT.emitCNFTM {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (clss : List (List (LitDesc n))) : TM n

Emit a CNF: fold clause emitters.

Equations

• Complexity.SAT.emitCNFTM rA rB rC rD tmp tmp2 clss = Complexity.TM.bigSeqTM (List.map (Complexity.SAT.emitClauseTM rA rB rC rD tmp tmp2) clss)

def Complexity.SAT.cnfBudget (K L M : ℕ) : ℕ

Time budget of a CNF emitter: K clauses of at most L literals.

Equations

• Complexity.SAT.cnfBudget K L M = K * (Complexity.SAT.clauseBudget L M + 1) + 1

theorem Complexity.SAT.emitCNFTM_hoareTime {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) {M A B C D : ℕ} (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) (inp₀ : Tape) (hinp₀ : TM.Parked inp₀) {clss : List (List (LitDesc n))} {φ : CNF} {work₀ : Fin n → Tape} : List.Forall₂ (fun (descs : List (LitDesc n)) (cl : List Lit) => List.Forall₂ (LitDesc.Spec work₀ tmp tmp2 M A B C D) descs cl) clss φ → ∀ {L : ℕ}, (∀ descs ∈ clss, descs.length ≤ L) → ∀ (ys : List Bool), (∀ (i : Fin n), TM.Parked (work₀ i)) → work₀ rA = TM.regTape A → work₀ rB = TM.regTape B → work₀ rC = TM.regTape C → work₀ rD = TM.regTape D → (emitCNFTM rA rB rC rD tmp tmp2 clss).HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch work₀ tmp tmp2 0) (ys ++ φ.encode)) (cnfBudget clss.length L M)

emitCNFTM Hoare specification: appends CNF.encode φ, scratches 0 to 0.