Parsimony of the actual paired-port compiler

For width-three inputs with at most three literal occurrences per variable, every satisfying source assignment has a satisfying output extension. Its values on the occurring output variables are uniquely determined by the source assignment. Conversely, reading the ordinary source cells recovers the source assignment. Counts use only occurring variables on both sides.

Main results

• sourceVariable_mem_rawFormula: every used source representative occurs in the actual output.
• raw_assignments_agree_iff: source and output agreement coincide for satisfying assignments.
• exists_satisfying_extension: every satisfying source assignment has an output extension.
• modelCount_rawFormula, modelCount_formula: the actual compiler preserves model counts.
• satisfiable_formula_iff: the corresponding satisfiability equivalence.

References

These are original counting and assignment-correspondence proofs for PairedCompile.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.source_cell_mem_ordinary {φ : Logic.PL.CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) : Orthogonal.Layout.center (List.idxOf v φ.distinctVars) ∈ ordinaryCells φ

Every used source cell is retained and receives an ordinary ring.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.sourceVariable_mem_rawFormula {φ : Logic.PL.CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) : (Orthogonal.Layout.center (List.idxOf v φ.distinctVars), Sum.inl (0, 0)) ∈ (rawFormula φ).vars

Every used source representative is an occurring variable of the actual raw output.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.raw_assignments_agree {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {σ τ : Variable → Bool} (hσ : Logic.PL.CNF.eval σ (rawFormula φ) = true) (hτ : Logic.PL.CNF.eval τ (rawFormula φ) = true) (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v) (v : Variable) : v ∈ (rawFormula φ).vars → σ v = τ v

Source agreement determines every occurring raw output variable. Assignments outside the formula's variable support are unrestricted.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.raw_assignments_agree_iff {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {σ τ : Variable → Bool} (hσ : Logic.PL.CNF.eval σ (rawFormula φ) = true) (hτ : Logic.PL.CNF.eval τ (rawFormula φ) = true) : (∀ v ∈ (rawFormula φ).vars, σ v = τ v) ↔ ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v

Among satisfying assignments, agreement on raw variables is equivalent to agreement on the occurring source variables read at their fixed source representatives.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.exists_satisfying_extension {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) (τ : ℕ → Bool) (hτ : Logic.PL.CNF.eval τ φ = true) : ∃ (σ : Variable → Bool), Logic.PL.CNF.eval σ (rawFormula φ) = true ∧ ∀ v ∈ φ.vars, sourceValue φ σ v = τ v

Every satisfying source assignment extends to a satisfying raw output assignment with the same source values. Together with raw_assignments_agree_iff, its occurring values are unique.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.modelCount_rawFormula (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (rawFormula φ).modelCount = φ.modelCount

The actual raw compiler preserves satisfying-assignment counts under the source width and literal-occurrence restrictions. Both sides count only occurring variables.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.modelCount_formula (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (formula φ).modelCount = φ.modelCount

Compact natural-number labels preserve the raw compiler's exact model count.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.satisfiable_formula_iff (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (formula φ).Satisfiable ↔ φ.Satisfiable

The actual compact compiler preserves satisfiability under the source restrictions.