From 209dd3ccc7be1f309c171f01ecb2e3e9321952d1 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:26:47 -0400 Subject: [PATCH 1/2] doc(roadmap): record ASP framework follow-up --- ROADMAP.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ROADMAP.md b/ROADMAP.md index e8aa6b0e1..2bdc7c2a8 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -187,6 +187,8 @@ index links to canonical definitions rather than keeping a second set. ### Counting and modular classes +- The Another Solution Problem (ASP) framework: solution-preserving reductions with explicit + polynomial-time solution bijections, and applications to SAT and planar SAT. - Counting reductions and further oracle results preserving exact multiplicities; permanent #P-completeness; modular and counting hierarchies; the oracle-algorithm form of Stockmeyer's approximate counting. From 5b65c48394bf529138806b0cfe2d571b797998e8 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:26:47 -0400 Subject: [PATCH 2/2] feat(CNF): preserve model counts under occurrence splitting Part of #1144, split from the internally reviewed parsimonious planar SAT development. All six local validation gates and hygiene checks pass. No selected abstract changes. AI-assisted implementation and internal review with Codex gpt-6.1-sol; outside-fleet coordinator review remains required. --- Complexity.lean | 5 + .../Complexity/Problems/ThreeSATThree.lean | 9 ++ .../Problems/ThreeSATThree/Counting.lean | 75 ++++++++++ Complexity/Foundations/Data/List/Filter.lean | 136 ++++++++++++++++++ Complexity/Foundations/Data/List/Last.lean | 40 ++++++ Complexity/Foundations/Data/List/Range.lean | 36 +++++ .../Propositional/CNF/Compact/ModelCount.lean | 58 ++++++++ .../Logics/Propositional/CNF/Occurrence.lean | 6 + .../Propositional/CNF/ThreeOccurrence.lean | 91 ++++++++++-- ComplexityTests/ThreeSATThreeCounting.lean | 64 +++++++++ 10 files changed, 507 insertions(+), 13 deletions(-) create mode 100644 Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean create mode 100644 Complexity/Foundations/Data/List/Filter.lean create mode 100644 Complexity/Foundations/Data/List/Last.lean create mode 100644 Complexity/Foundations/Data/List/Range.lean create mode 100644 Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean create mode 100644 ComplexityTests/ThreeSATThreeCounting.lean diff --git a/Complexity.lean b/Complexity.lean index e6c16467f..55ff7de36 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -828,6 +828,7 @@ public import Complexity.Computability.Complexity.Problems.TQBF.Closed public import Complexity.Computability.Complexity.Problems.TSP public import Complexity.Computability.Complexity.Problems.ThreeSAT public import Complexity.Computability.Complexity.Problems.ThreeSATThree +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax public import Complexity.Computability.Complexity.Problems.TwoSAT @@ -1886,10 +1887,13 @@ public import Complexity.Foundations.Data.List.BalancedFold public import Complexity.Foundations.Data.List.Basic public import Complexity.Foundations.Data.List.Counting public import Complexity.Foundations.Data.List.Equiv +public import Complexity.Foundations.Data.List.Filter public import Complexity.Foundations.Data.List.Fold +public import Complexity.Foundations.Data.List.Last public import Complexity.Foundations.Data.List.Lex public import Complexity.Foundations.Data.List.Lookup public import Complexity.Foundations.Data.List.OfFn +public import Complexity.Foundations.Data.List.Range public import Complexity.Foundations.Data.List.SelectDistinct public import Complexity.Foundations.Data.Matrix.Binary public import Complexity.Foundations.Data.Matrix.Permanent @@ -2080,6 +2084,7 @@ public import Complexity.Logics.FirstOrder.Tuple public import Complexity.Logics.Propositional.CNF public import Complexity.Logics.Propositional.CNF.Coding public import Complexity.Logics.Propositional.CNF.Compact +public import Complexity.Logics.Propositional.CNF.Compact.ModelCount public import Complexity.Logics.Propositional.CNF.Compact.Relabel public import Complexity.Logics.Propositional.CNF.ExactlyOne public import Complexity.Logics.Propositional.CNF.Gadgets diff --git a/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean b/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean index bfa06d5a0..b2cbc9f37 100644 --- a/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean +++ b/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean @@ -42,6 +42,7 @@ This endpoint imposes no planarity condition. ## Main results * `Cslib.Complexity.mem_ThreeSATThree_toThreeSATThree_iff`: correctness of the reduction. +* `Cslib.Complexity.modelCount_toThreeSATThree`: preservation of counts for width-three inputs. * `Cslib.Complexity.computableInPolyTime_toThreeSATThree`: native polynomial time under `encCNF`. * `Cslib.Complexity.ThreeSATThree_npComplete`: 3SAT-3 is NP-complete. @@ -149,6 +150,14 @@ theorem length_vars_toThreeSATThree (φ : CNF ℕ) (hφ : ∀ c ∈ φ, c.length have hg : φ.all (fun c => decide (c.length ≤ 3)) = true := by simpa using hφ simp [toThreeSATThree, hg, CNF.vars_relabel, CNF.length_vars_toThreeOccurrence] +/-- For a width-three input, occurrence splitting and injective numbering preserve the number of +satisfying assignments on occurring variables. -/ +theorem modelCount_toThreeSATThree (φ : CNF ℕ) (hφ : ∀ c ∈ φ, c.length ≤ 3) : + (toThreeSATThree φ).modelCount = φ.modelCount := by + have hg : φ.all (fun c => decide (c.length ≤ 3)) = true := by simpa using hφ + simp only [toThreeSATThree, hg, ↓reduceIte] + rw [CNF.modelCount_relabel ThreeSATThree.numberCopy_injective, CNF.modelCount_toThreeOccurrence] + /-- The total splitter is polynomial-time under binary `encCNF`. -/ @[fun_prop] theorem computableInPolyTime_toThreeSATThree : diff --git a/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean b/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean new file mode 100644 index 000000000..b6e9f2dbe --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.SharpP.Completeness +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax + +/-! +# Parsimonious occurrence reduction for 3SAT + +The existing occurrence splitter preserves the number of satisfying assignments. Each source +variable has one value on every copy in its implication cycle, and numbering copies is injective. +The counting problems below count only occurring variables and return zero outside their syntax. +They reuse `CNF.modelCount` and the existing syntax guards rather than introducing new assignment +or satisfiability semantics. + +## Main definitions + +* `Cslib.Complexity.SharpThreeSAT`: model count for width-at-most-three CNF, zero otherwise. +* `Cslib.Complexity.SharpThreeSATThree`: model count with the additional three-occurrence bound. + +## Main results + +* `Cslib.Complexity.sharpThreeSATThree_toThreeSATThree`: exact counts for the total compiler. +* `Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree`: the existing + polynomial-time compiler is a parsimonious reduction. + +## References + +The occurrence construction and its source credit are documented in `ThreeSATThree`. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Cslib.Logic.PL + +/-- Count satisfying assignments of width-at-most-three CNF; reject other syntax with count zero. +Only variables occurring in the formula are counted. -/ +def SharpThreeSAT (φ : CNF ℕ) : ℕ := + if φ.all (fun c => decide (c.length ≤ 3)) then φ.modelCount else 0 + +/-- Count satisfying assignments of width-three, occurrence-three CNF; reject other syntax with +count zero. Repetitions are literal positions, as in `ThreeSATThree.syntaxCheck`. -/ +def SharpThreeSATThree (φ : CNF ℕ) : ℕ := + if ThreeSATThree.syntaxCheck φ then φ.modelCount else 0 + +/-- The total occurrence compiler preserves the count, including rejected inputs. -/ +theorem sharpThreeSATThree_toThreeSATThree (φ : CNF ℕ) : + SharpThreeSATThree (toThreeSATThree φ) = SharpThreeSAT φ := by + have hout := (ThreeSATThree.syntaxCheck_iff (toThreeSATThree φ)).2 + ⟨width_toThreeSATThree φ, count_vars_toThreeSATThree_le φ⟩ + simp only [SharpThreeSATThree, hout, ↓reduceIte] + by_cases hw : φ.all (fun c => decide (c.length ≤ 3)) = true + · have hwidth : ∀ c ∈ φ, c.length ≤ 3 := by + simpa only [List.all_eq_true, decide_eq_true_eq] using hw + rw [modelCount_toThreeSATThree φ hwidth] + simp only [SharpThreeSAT, hw, ↓reduceIte] + · simp only [SharpThreeSAT, toThreeSATThree, hw, Bool.false_eq_true, ite_false] + decide + +/-- The already-certified polynomial-time 3SAT-to-3SAT-3 compiler is parsimonious. -/ +theorem parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree : + ParsimoniousReducible encCNF encCNF SharpThreeSAT SharpThreeSATThree := + ⟨toThreeSATThree, computableInPolyTime_toThreeSATThree, + fun φ => (sharpThreeSATThree_toThreeSATThree φ).symm⟩ + +end Cslib.Complexity diff --git a/Complexity/Foundations/Data/List/Filter.lean b/Complexity/Foundations/Data/List/Filter.lean new file mode 100644 index 000000000..1af02195a --- /dev/null +++ b/Complexity/Foundations/Data/List/Filter.lean @@ -0,0 +1,136 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Init +import Mathlib.Data.List.GetD + +/-! +# Indexed multiplicity under list membership filtering + +These statements count positions, so repeated equal lists still contribute separately. +They are generalized from the canonical incidence-path occupancy proofs. + +## Main results + +* `List.exists_pair_indices_of_two_le_filter_contains`. +* `List.two_le_filter_contains_of_indices`. +* `List.exists_other_index_of_two_le_filter_contains`. +-/ + +@[expose] public section + +namespace List + +/-- Two filtered memberships occur at distinct indices, even for repeated lists. -/ +theorem exists_pair_indices_of_two_le_filter_contains {α : Type*} [DecidableEq α] + (rs : List (List α)) (p : α) + (hlen : 2 ≤ (rs.filter fun r => r.contains p).length) : + ∃ (i j : ℕ) (hi : i < rs.length) (hj : j < rs.length), + i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j] := by + induction rs with + | nil => simp at hlen + | cons r rs ih => + by_cases hp : p ∈ r + · have hne : (rs.filter fun r => r.contains p) ≠ [] := by + intro h + have hf : ((r :: rs).filter fun r => r.contains p) = [r] := by + have hpred : r.contains p = true := by simpa using hp + simp only [List.filter_cons, hpred, ↓reduceIte, h] + rw [hf] at hlen + simp at hlen + cases hf : rs.filter (fun r => r.contains p) with + | nil => exact False.elim (hne hf) + | cons t ts => + have ht : t ∈ rs.filter (fun r => r.contains p) := by rw [hf]; simp + obtain ⟨htmem, htp⟩ := List.mem_filter.mp ht + obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp htmem + exact ⟨0, j + 1, by simp, by simpa using hj, by omega, hp, by simpa using htp⟩ + · have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by + simp [hp] + rw [hf] at hlen + obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := ih hlen + exact ⟨i + 1, j + 1, by simpa using hi, by simpa using hj, by omega, hpi, hpj⟩ + +/-- Two distinct indices witnessing membership give at least two filtered entries. -/ +theorem two_le_filter_contains_of_indices {α : Type*} [DecidableEq α] + (rs : List (List α)) (p : α) {i j : ℕ} + (hi : i < rs.length) (hj : j < rs.length) (hij : i ≠ j) + (hpi : p ∈ rs[i]) (hpj : p ∈ rs[j]) : + 2 ≤ (rs.filter fun r => r.contains p).length := by + induction rs generalizing i j with + | nil => simp at hi + | cons r rs ih => + cases i with + | zero => + cases j with + | zero => exact False.elim (hij rfl) + | succ j => + have hj' : j < rs.length := by simpa using hj + have hm : rs[j] ∈ rs.filter (fun r => r.contains p) := + List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hj), + List.contains_iff_mem.mpr hpj⟩ + obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm + have hphead : p ∈ r := hpi + simp only [List.filter_cons, List.contains_iff_mem.mpr hphead, + ite_true, List.length_cons] + omega + | succ i => + cases j with + | zero => + have hi' : i < rs.length := by simpa using hi + have hm : rs[i] ∈ rs.filter (fun r => r.contains p) := + List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hi), + List.contains_iff_mem.mpr hpi⟩ + obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm + have hphead : p ∈ r := hpj + simp only [List.filter_cons, List.contains_iff_mem.mpr hphead, + ite_true, List.length_cons] + omega + | succ j => + have ht := ih (by simpa using hi) (by simpa using hj) (by omega) hpi hpj + rw [List.filter_cons] + split_ifs + · simp only [List.length_cons] + omega + · exact ht + +/-- At least two filtered memberships give an index different from any given index. -/ +theorem exists_other_index_of_two_le_filter_contains {α : Type*} [DecidableEq α] + (rs : List (List α)) (p : α) (i : ℕ) (hi : i < rs.length) + (hcount : 2 ≤ (rs.filter fun r => r.contains p).length) : + ∃ j, ∃ hj : j < rs.length, j ≠ i ∧ p ∈ rs[j] := by + induction rs generalizing i with + | nil => simp at hi + | cons r rs ih => + cases i with + | zero => + have hpos : 0 < (rs.filter fun r => r.contains p).length := by + rw [List.filter_cons] at hcount + split_ifs at hcount + · simp only [List.length_cons] at hcount + omega + · omega + obtain ⟨s, hs⟩ := List.exists_mem_of_length_pos hpos + have hm := List.mem_filter.mp hs + obtain ⟨j, hj, hsj⟩ := List.mem_iff_getElem.mp hm.1 + refine ⟨j + 1, by simp only [List.length_cons]; omega, by omega, ?_⟩ + simp only [List.getElem_cons_succ] + rw [hsj] + exact List.contains_iff_mem.mp hm.2 + | succ i => + by_cases hmem : r.contains p = true + · exact ⟨0, by simp, by omega, by simpa using List.contains_iff_mem.mp hmem⟩ + · have ht : 2 ≤ (rs.filter fun r => r.contains p).length := by + have hp : p ∉ r := fun hp => hmem (List.contains_iff_mem.mpr hp) + simpa [List.filter_cons, hp] using hcount + obtain ⟨j, hj, hji, hp⟩ := ih i (by simp only [List.length_cons] at hi; omega) ht + exact ⟨j + 1, by simp only [List.length_cons]; omega, by omega, by simpa using hp⟩ + + +end List diff --git a/Complexity/Foundations/Data/List/Last.lean b/Complexity/Foundations/Data/List/Last.lean new file mode 100644 index 000000000..b0781335c --- /dev/null +++ b/Complexity/Foundations/Data/List/Last.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Init +import Mathlib.Data.List.GetD + +/-! +# Defaulted last-element lookup + +The default is unused for a nonempty list. The proof is moved from the path semantics. + +## Main results + +* `List.getLastD_eq_getElem`. +-/ + +@[expose] public section + +namespace List + +/-- A nonempty list's defaulted last lookup is its final indexed element. -/ +theorem getLastD_eq_getElem {α : Type*} (xs : List α) (d : α) (hne : xs ≠ []) : + xs.getLastD d = xs[xs.length - 1]'(by cases xs <;> simp_all) := by + induction xs generalizing d with + | nil => exact False.elim (hne rfl) + | cons a xs ih => + cases xs with + | nil => rfl + | cons b xs => + rw [List.getLastD_cons, ih a (List.cons_ne_nil _ _)] + simp only [List.length_cons, Nat.add_sub_cancel, List.getElem_cons_succ] + + +end List diff --git a/Complexity/Foundations/Data/List/Range.lean b/Complexity/Foundations/Data/List/Range.lean new file mode 100644 index 000000000..d2770bd73 --- /dev/null +++ b/Complexity/Foundations/Data/List/Range.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Init +import Mathlib.Data.List.GetD +import Mathlib.Data.List.Nodup + +/-! +# First indices in natural-number ranges + +This index identity is shared by source endpoint and path geometry certificates. + +## Main results + +* `List.idxOf_range_of_lt`. +-/ + +@[expose] public section + +namespace List + +/-- An in-range natural number occurs at its own position in `range`. -/ +theorem idxOf_range_of_lt {i n : ℕ} (hi : i < n) : (List.range n).idxOf i = i := by + have h := (List.nodup_range : (List.range n).Nodup).idxOf_getElem i + (by simpa only [List.length_range] using hi) + rw [List.getElem_range] at h + exact h + + +end List diff --git a/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean b/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean new file mode 100644 index 000000000..83e40eca3 --- /dev/null +++ b/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean @@ -0,0 +1,58 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.CNF.Compact +public import Complexity.Logics.Propositional.CNF.ModelCount +import Mathlib.Data.List.GetD + +/-! +# Model counts under compact variable numbering + +First-occurrence numbering preserves the number of satisfying assignments on the variables +occurring in a formula. The variable type may be infinite or empty. + +## Main results + +* `Cslib.Logic.PL.CNF.modelCount_compact`: compaction preserves the model count. + +## References + +This is an elementary counting property of the existing compaction construction. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF + +variable {V : Type*} [DecidableEq V] + +/-- First-occurrence numbering preserves the number of satisfying assignments, including for +empty formulas, empty clauses, and repeated literal occurrences. -/ +theorem modelCount_compact (φ : CNF V) : φ.compact.modelCount = φ.modelCount := by + refine modelCount_eq_card_filter (fun σ (v : φ.vars.toFinset) => σ (φ.vars.idxOf (v : V))) + (fun τ => φ.eval (φ.extendAssignment τ) = true) (fun σ τ _ _ => ?_) fun τ => ?_ + · rw [compact, vars_relabel, List.forall_mem_map, funext_iff, Subtype.forall] + simp only [List.mem_toFinset] + · constructor + · intro hτ + let σ : ℕ → Bool := fun i => φ.vars[i]?.elim false (φ.extendAssignment τ) + have he : ∀ v ∈ φ.vars, σ (φ.vars.idxOf v) = φ.extendAssignment τ v := by + intro v hv + simp [σ, List.getElem?_idxOf hv] + refine ⟨σ, ?_, funext fun v => ?_⟩ + · rw [compact, eval_relabel] + exact (eval_congr he).trans hτ + · exact (he v (List.mem_toFinset.1 v.2)).trans + (extendAssignment_of_mem _ (List.mem_toFinset.1 v.2)) + · rintro ⟨σ, hσ, rfl⟩ + rw [compact, eval_relabel] at hσ + rw [← hσ] + exact eval_extendAssignment_restrict φ (σ ∘ φ.vars.idxOf) + +end Cslib.Logic.PL.CNF diff --git a/Complexity/Logics/Propositional/CNF/Occurrence.lean b/Complexity/Logics/Propositional/CNF/Occurrence.lean index 8d299e11d..17ba7e0ba 100644 --- a/Complexity/Logics/Propositional/CNF/Occurrence.lean +++ b/Complexity/Logics/Propositional/CNF/Occurrence.lean @@ -24,6 +24,12 @@ The proof follows the indexed-copy uniqueness argument in `CNF.ThreeOccurrence`. namespace Cslib.Logic.PL +/-- The variable named by an indexed literal occurrence occurs in the formula. -/ +theorem variable_mem_of_mem_occurrences {V : Type*} {φ : CNF V} {o : Occurrence V} + (ho : o ∈ occurrences φ) : o.2.2.1 ∈ φ.vars := by + rw [← map_occurrences] + exact List.mem_map_of_mem ho + /-- Clause and literal indices distinguish every source occurrence, including repeated literals. -/ theorem occurrences_nodup {V : Type*} (φ : CNF V) : (occurrences φ).Nodup := by rw [occurrences, List.nodup_flatMap] diff --git a/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean b/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean index edd3bb974..9c714a4f0 100644 --- a/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean +++ b/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean @@ -35,7 +35,9 @@ This construction uses ordinary CNF formulas and Boolean assignments. ## Main results +* `Cslib.Logic.PL.CNF.eval_toThreeOccurrence_iff`: correspondence of satisfying assignments. * `Cslib.Logic.PL.CNF.satisfiable_toThreeOccurrence`: equisatisfiability. +* `Cslib.Logic.PL.CNF.modelCount_toThreeOccurrence`: preservation of satisfying-assignment counts. * `Cslib.Logic.PL.CNF.width_toThreeOccurrence`: preservation of width bounds of at least two. * `Cslib.Logic.PL.CNF.count_vars_toThreeOccurrence_le`: at most three literal occurrences. * `Cslib.Logic.PL.CNF.length_toThreeOccurrence`, @@ -114,11 +116,14 @@ theorem copies_agree [DecidableEq V] {φ : CNF V} {τ : V × ℕ × ℕ → Bool · simp [occurrenceCopies, hx] · simp [occurrenceCopies, hy, he] -/-- Occurrence splitting preserves satisfiability, including empty clauses and formulas. -/ -theorem satisfiable_toThreeOccurrence [DecidableEq V] (φ : CNF V) : - φ.toThreeOccurrence.Satisfiable ↔ φ.Satisfiable := by +/-- An assignment satisfies the split formula exactly when its occurring copies agree with a +satisfying assignment of the original formula. Together with `copies_agree`, this retains the +assignment correspondence, rather than just equisatisfiability. -/ +theorem eval_toThreeOccurrence_iff [DecidableEq V] (φ : CNF V) (τ : V × ℕ × ℕ → Bool) : + φ.toThreeOccurrence.eval τ = true ↔ + ∃ σ : V → Bool, φ.eval σ = true ∧ ∀ x ∈ φ.occurrenceClauses.vars, σ x.1 = τ x := by constructor - · rintro ⟨τ, hτ⟩ + · intro hτ classical let σ : V → Bool := fun v => if h : ∃ x ∈ φ.occurrenceClauses.vars, x.1 = v then τ (Classical.choose h) else false @@ -127,21 +132,33 @@ theorem satisfiable_toThreeOccurrence [DecidableEq V] (φ : CNF V) : have hex : ∃ y ∈ φ.occurrenceClauses.vars, y.1 = x.1 := ⟨x, hx, rfl⟩ simp only [σ, dite_eq_left hex] exact copies_agree hτ (Classical.choose_spec hex).1 hx (Classical.choose_spec hex).2 - refine ⟨σ, ?_⟩ + refine ⟨σ, ?_, he⟩ rw [← eval_occurrenceClauses] have ht := hτ simp only [toThreeOccurrence, eval_append, Bool.and_eq_true] at ht exact (eval_congr he).trans ht.1 - · rintro ⟨σ, hσ⟩ - refine ⟨σ ∘ Prod.fst, ?_⟩ - rw [toThreeOccurrence, eval_append, Bool.and_eq_true, eval_occurrenceClauses] - refine ⟨hσ, (eval_flatMap_eq_true_iff _ _ _).2 fun v _ => ?_⟩ + · rintro ⟨σ, hσ, he⟩ + rw [toThreeOccurrence, eval_append, Bool.and_eq_true] + refine ⟨(eval_congr he).symm.trans ((eval_occurrenceClauses φ σ).trans hσ), + (eval_flatMap_eq_true_iff _ _ _).2 fun v _ => ?_⟩ rw [eval_implicationCycle] intro x hx y hy - have hx := (List.mem_filter.1 hx).2 - have hy := (List.mem_filter.1 hy).2 - simp only [beq_iff_eq] at hx hy - simp [hx, hy] + obtain ⟨hx, hxv⟩ := List.mem_filter.1 hx + obtain ⟨hy, hyv⟩ := List.mem_filter.1 hy + simp only [beq_iff_eq] at hxv hyv + calc τ x = σ x.1 := (he x hx).symm + _ = σ y.1 := congrArg σ (hxv.trans hyv.symm) + _ = τ y := he y hy + +/-- Occurrence splitting preserves satisfiability, including empty clauses and formulas. -/ +theorem satisfiable_toThreeOccurrence [DecidableEq V] (φ : CNF V) : + φ.toThreeOccurrence.Satisfiable ↔ φ.Satisfiable := by + constructor + · rintro ⟨τ, hτ⟩ + obtain ⟨σ, hσ, _⟩ := (eval_toThreeOccurrence_iff φ τ).1 hτ + exact ⟨σ, hσ⟩ + · rintro ⟨σ, hσ⟩ + exact ⟨σ ∘ Prod.fst, (eval_toThreeOccurrence_iff φ _).2 ⟨σ, hσ, fun _ _ => rfl⟩⟩ /-- Cycles are binary, so a width bound of at least two is preserved. -/ theorem width_toThreeOccurrence [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : 2 ≤ k) @@ -271,4 +288,52 @@ theorem numVars_toThreeOccurrence [DecidableEq V] (φ : CNF V) : rw [numVars, he, List.toFinset_card_of_nodup (nodup_vars_occurrenceClauses φ)] simpa using congrArg List.length (map_fst_vars_occurrenceClauses φ) +/-- Occurrence splitting preserves the number of satisfying assignments on occurring variables, +including empty formulas, empty clauses, and repeated literals. -/ +theorem modelCount_toThreeOccurrence [DecidableEq V] (φ : CNF V) : + φ.toThreeOccurrence.modelCount = φ.modelCount := by + classical + have hmem (x : V × ℕ × ℕ) : + x ∈ φ.toThreeOccurrence.vars ↔ x ∈ φ.occurrenceClauses.vars := by + simp only [← List.count_pos_iff, count_vars_toThreeOccurrence] + omega + have hfst {x : V × ℕ × ℕ} (hx : x ∈ φ.occurrenceClauses.vars) : x.1 ∈ φ.vars := by + rw [← map_fst_vars_occurrenceClauses] + exact List.mem_map.2 ⟨x, hx, rfl⟩ + have hex (v : φ.vars.toFinset) : ∃ x ∈ φ.occurrenceClauses.vars, x.1 = v := by + apply List.mem_map.1 + simpa only [map_fst_vars_occurrenceClauses] using List.mem_toFinset.1 v.2 + let copy (v : φ.vars.toFinset) : V × ℕ × ℕ := Classical.choose (hex v) + have hcopy (v : φ.vars.toFinset) : copy v ∈ φ.occurrenceClauses.vars ∧ (copy v).1 = v := + Classical.choose_spec (hex v) + let f (τ : V × ℕ × ℕ → Bool) (v : φ.vars.toFinset) : Bool := τ (copy v) + refine modelCount_eq_card_filter f (fun τ => φ.eval (φ.extendAssignment τ) = true) + (fun σ τ hσ hτ => ?_) fun τ => ?_ + · constructor + · intro he x hx + have hx := (hmem x).1 hx + let v : φ.vars.toFinset := ⟨x.1, List.mem_toFinset.2 (hfst hx)⟩ + calc σ x = σ (copy v) := copies_agree hσ hx (hcopy v).1 (hcopy v).2.symm + _ = τ (copy v) := congrFun he v + _ = τ x := copies_agree hτ (hcopy v).1 hx (hcopy v).2 + · intro he + exact funext fun v => he (copy v) ((hmem _).2 (hcopy v).1) + · constructor + · intro hτ + refine ⟨φ.extendAssignment τ ∘ Prod.fst, ?_, funext fun v => ?_⟩ + · exact (eval_toThreeOccurrence_iff φ _).2 ⟨φ.extendAssignment τ, hτ, fun _ _ => rfl⟩ + · change φ.extendAssignment τ (copy v).1 = τ v + rw [(hcopy v).2, extendAssignment_of_mem _ (List.mem_toFinset.1 v.2)] + · rintro ⟨σ, hσ, rfl⟩ + rw [← eval_occurrenceClauses] + have he : ∀ x ∈ φ.occurrenceClauses.vars, + (φ.extendAssignment (f σ) ∘ Prod.fst) x = σ x := by + intro x hx + change φ.extendAssignment (f σ) x.1 = σ x + rw [extendAssignment_of_mem _ (hfst hx)] + exact copies_agree hσ (hcopy _).1 hx (hcopy _).2 + have ht := hσ + simp only [toThreeOccurrence, eval_append, Bool.and_eq_true] at ht + exact (eval_congr he).trans ht.1 + end Cslib.Logic.PL.CNF diff --git a/ComplexityTests/ThreeSATThreeCounting.lean b/ComplexityTests/ThreeSATThreeCounting.lean new file mode 100644 index 000000000..270dafc50 --- /dev/null +++ b/ComplexityTests/ThreeSATThreeCounting.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Computability.Complexity.Problems.ThreeSATThree +import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting + +/-! # Exact counts under occurrence splitting and numbering -/ + +open Cslib.Logic.PL Cslib.Complexity + +/-- The empty formula has one assignment on its empty variable set. -/ +example : (toThreeSATThree []).modelCount = 1 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- An empty clause has no satisfying assignment. -/ +example : (toThreeSATThree [[]]).modelCount = 0 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- Repeated literals within a clause do not multiply the satisfying-assignment count. -/ +example : (toThreeSATThree [[(0, true), (0, true), (0, true)]]).modelCount = 1 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- A singleton cycle introduces no additional choice for a forced variable. -/ +example : (toThreeSATThree [[(7, true)]]).modelCount = 1 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- Several occurrences per variable preserve all three satisfying assignments of a disjunction. -/ +example : (toThreeSATThree + [[(0, true), (1, true)], [(0, true), (1, true)]]).modelCount = 3 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- The unnumbered splitter preserves counts even beyond width three. -/ +example : (CNF.toThreeOccurrence + [[(0, true), (0, false), (0, true), (0, false)]]).modelCount = 2 := by + rw [CNF.modelCount_toThreeOccurrence] + decide + +/-- The numbered reduction rejects a width-four input, so its width hypothesis is necessary. -/ +example : (toThreeSATThree + [[(0, true), (0, false), (0, true), (0, false)]]).modelCount = 0 := by + decide + +/-- A satisfiable width-four formula has raw models but is rejected by the 3SAT count. -/ +example : SharpThreeSAT [[(0, true), (0, false), (0, true), (0, false)]] = 0 := by decide + +/-- The source count accepts width three even when the occurrence bound fails. -/ +example : SharpThreeSAT [[(0, true), (0, true), (0, true)], [(0, true)]] = 1 := by decide + +/-- The target count rejects the same formula for its fourth literal occurrence. -/ +example : SharpThreeSATThree [[(0, true), (0, true), (0, true)], [(0, true)]] = 0 := by decide + +/-- The actual compiler preserves that source count after repairing the occurrence bound. -/ +example : SharpThreeSATThree + (toThreeSATThree [[(0, true), (0, true), (0, true)], [(0, true)]]) = 1 := by + rw [sharpThreeSATThree_toThreeSATThree] + decide