From fc349c87053acdbc2f2b4abe2e247272fd447faf Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 01:01:37 +0000 Subject: [PATCH 1/2] feat(logic): satisfiability of clause sets ClauseSet.Satisfiable (decidable over finite variables), satisfiable_toCNF_iff, sat_*_iff lemmas for combined clause sets, and ClauseSet.relabel with satisfiable_relabel, mirroring CNF.relabel. Replaces the private sat_union_iff in Sparsification/Counting. First PR of #1599. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Propositional/ClauseSet/Satisfiable.lean | 154 ++++++++++++++++++ .../ClauseSet/Sparsification/Counting.lean | 9 +- ComplexityTests/ClauseSetSatisfiable.lean | 63 +++++++ 4 files changed, 219 insertions(+), 8 deletions(-) create mode 100644 Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean create mode 100644 ComplexityTests/ClauseSetSatisfiable.lean diff --git a/Complexity.lean b/Complexity.lean index f08f52b9d..1727af0d1 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2974,6 +2974,7 @@ public import Complexity.Logics.Propositional.CSP.ToBoolean public import Complexity.Logics.Propositional.CSP.ToCNF public import Complexity.Logics.Propositional.CSP.ToCNF.Count public import Complexity.Logics.Propositional.ClauseSet.Basic +public import Complexity.Logics.Propositional.ClauseSet.Satisfiable public import Complexity.Logics.Propositional.ClauseSet.Sparsification public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Bounds public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting diff --git a/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean b/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean new file mode 100644 index 000000000..c8375400a --- /dev/null +++ b/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean @@ -0,0 +1,154 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.ClauseSet.Basic + +/-! +# Satisfiability of clause sets + +A clause set is *satisfiable* when some assignment satisfies all of its clauses +(`ClauseSet.Satisfiable`). Over a finite type of variables this is decidable, and it agrees with +satisfiability of a formula listing the clauses (`ClauseSet.satisfiable_toCNF_iff`). Satisfaction +of unions, insertions, images and indexed unions of clause sets is characterized clause by clause, +and renaming the variables along an injective map preserves satisfiability +(`ClauseSet.satisfiable_relabel`), as for formulas (`CNF.satisfiable_relabel`). + +## Main definitions + +* `Cslib.Logic.PL.ClauseSet.Satisfiable`: some assignment satisfies every clause. +* `Cslib.Logic.PL.ClauseSet.relabel`: rename the variables of a clause set. + +## Main results + +* `Cslib.Logic.PL.ClauseSet.satisfiable_toCNF_iff`: agreement with `CNF.Satisfiable`. +* `Cslib.Logic.PL.ClauseSet.sat_union_iff`, `Cslib.Logic.PL.ClauseSet.sat_insert_iff`, + `Cslib.Logic.PL.ClauseSet.sat_singleton_iff`, `Cslib.Logic.PL.ClauseSet.sat_empty`, + `Cslib.Logic.PL.ClauseSet.sat_image_iff`, `Cslib.Logic.PL.ClauseSet.sat_biUnion_iff`: + satisfaction of combined clause sets. +* `Cslib.Logic.PL.ClauseSet.sat_relabel_iff`, `Cslib.Logic.PL.ClauseSet.satisfiable_relabel`: + relabelling. +* `Cslib.Logic.PL.ClauseSet.relabel_union`, `Cslib.Logic.PL.ClauseSet.mem_relabel`: the clauses of + a relabelled clause set. +* `Cslib.Logic.PL.ClauseSet.card_relabel_le`, `Cslib.Logic.PL.ClauseSet.card_le_of_mem_relabel`: + relabelling adds neither clauses nor literals. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL + +open Finset + +namespace ClauseSet + +variable {V W ι : Type*} + +/-- Some assignment satisfies every clause of `ψ`. -/ +def Satisfiable (ψ : ClauseSet V) : Prop := + ∃ x : V → Bool, ψ.Sat x + +instance [Fintype V] [DecidableEq V] (ψ : ClauseSet V) : Decidable ψ.Satisfiable := + inferInstanceAs (Decidable (∃ x : V → Bool, ψ.Sat x)) + +/-- A clause set is satisfiable exactly when a formula listing its clauses is. -/ +theorem satisfiable_toCNF_iff (ψ : ClauseSet V) : ψ.toCNF.Satisfiable ↔ ψ.Satisfiable := by + simp only [CNF.Satisfiable, ClauseSet.eval_toCNF_eq_true_iff, Satisfiable] + +/-! ### Satisfaction of combined clause sets -/ + +section Sat + +variable {x : V → Bool} + +/-- An assignment satisfies a union exactly when it satisfies both parts. -/ +@[simp] theorem sat_union_iff [DecidableEq V] {ψ φ : ClauseSet V} : + (ψ ∪ φ).Sat x ↔ ψ.Sat x ∧ φ.Sat x := by + simp only [Sat, mem_union] + exact ⟨fun h => ⟨fun C hC => h C (Or.inl hC), fun C hC => h C (Or.inr hC)⟩, + fun ⟨h₁, h₂⟩ C hC => hC.elim (h₁ C) (h₂ C)⟩ + +/-- An assignment satisfies `insert C ψ` exactly when it satisfies the clause `C` and `ψ`. -/ +@[simp] theorem sat_insert_iff [DecidableEq V] {C : Finset (Literal V)} {ψ : ClauseSet V} : + (insert C ψ).Sat x ↔ (∃ l ∈ C, x l.1 = l.2) ∧ ψ.Sat x := by + simp [Sat] + +/-- An assignment satisfies a single clause exactly when it makes one of its literals true. -/ +@[simp] theorem sat_singleton_iff {C : Finset (Literal V)} : + ({C} : ClauseSet V).Sat x ↔ ∃ l ∈ C, x l.1 = l.2 := by + simp [Sat] + +/-- Every assignment satisfies the empty clause set. -/ +@[simp] theorem sat_empty : (∅ : ClauseSet V).Sat x := by + simp [Sat] + +/-- An assignment satisfies the clauses `f i` for `i ∈ s` exactly when it satisfies each. -/ +theorem sat_image_iff [DecidableEq V] {s : Finset ι} {f : ι → Finset (Literal V)} : + ClauseSet.Sat (s.image f) x ↔ ∀ i ∈ s, ∃ l ∈ f i, x l.1 = l.2 := by + simp [Sat] + +/-- An assignment satisfies an indexed union exactly when it satisfies each part. -/ +theorem sat_biUnion_iff [DecidableEq V] {s : Finset ι} {f : ι → ClauseSet V} : + ClauseSet.Sat (s.biUnion f) x ↔ ∀ i ∈ s, (f i).Sat x := by + simp only [Sat, mem_biUnion] + exact ⟨fun h i hi C hC => h C ⟨i, hi, hC⟩, fun h C ⟨i, hi, hC⟩ => h i hi C hC⟩ + +end Sat + +/-! ### Relabelling -/ + +section Relabel + +variable [DecidableEq W] + +/-- Rename the variables of a clause set along `f`. -/ +def relabel (f : V → W) (ψ : ClauseSet V) : ClauseSet W := + ψ.image fun C => C.image (Prod.map f id) + +/-- `σ` satisfies `ψ.relabel f` exactly when `σ ∘ f` satisfies `ψ`. -/ +@[simp] theorem sat_relabel_iff (f : V → W) (ψ : ClauseSet V) (σ : W → Bool) : + (ψ.relabel f).Sat σ ↔ ψ.Sat (σ ∘ f) := by + simp [relabel, Sat] + +/-- Relabelling along an injective map preserves satisfiability. An assignment of the new +variables restricts to the old ones, and an assignment of the old variables extends along `f`. -/ +theorem satisfiable_relabel {f : V → W} (hf : Function.Injective f) (ψ : ClauseSet V) : + (ψ.relabel f).Satisfiable ↔ ψ.Satisfiable := by + constructor + · rintro ⟨σ, hσ⟩ + exact ⟨σ ∘ f, (sat_relabel_iff f ψ σ).mp hσ⟩ + · rintro ⟨σ, hσ⟩ + refine ⟨Function.extend f σ fun _ => false, (sat_relabel_iff f ψ _).mpr ?_⟩ + rwa [Function.extend_comp hf] + +/-- Relabelling commutes with unions. -/ +theorem relabel_union [DecidableEq V] (f : V → W) (ψ φ : ClauseSet V) : + (ψ ∪ φ).relabel f = ψ.relabel f ∪ φ.relabel f := + image_union _ _ + +/-- Relabelling does not add clauses; it may merge some. -/ +theorem card_relabel_le (f : V → W) (ψ : ClauseSet V) : (ψ.relabel f).card ≤ ψ.card := + card_image_le + +/-- The clauses of `ψ.relabel f` are the images of the clauses of `ψ`. -/ +@[simp] theorem mem_relabel {f : V → W} {ψ : ClauseSet V} {C : Finset (Literal W)} : + C ∈ ψ.relabel f ↔ ∃ C' ∈ ψ, C'.image (Prod.map f id) = C := + mem_image + +/-- Relabelling does not widen clauses: if every clause of `ψ` has at most `k` literals, so does +every clause of `ψ.relabel f`. -/ +theorem card_le_of_mem_relabel {f : V → W} {ψ : ClauseSet V} {k : ℕ} + (hψ : ∀ C ∈ ψ, C.card ≤ k) {C : Finset (Literal W)} (hC : C ∈ ψ.relabel f) : C.card ≤ k := by + obtain ⟨C', hC', rfl⟩ := mem_relabel.mp hC + exact card_image_le.trans (hψ C' hC') + +end Relabel + +end ClauseSet + +end Cslib.Logic.PL diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/Counting.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/Counting.lean index 343a405cd..ffd7d51ee 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/Counting.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/Counting.lean @@ -9,6 +9,7 @@ module public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Step public import Complexity.Logics.Propositional.CNF.ModelCount.Declared +import Complexity.Logics.Propositional.ClauseSet.Satisfiable /-! # Disjoint sparsification branches @@ -53,14 +54,6 @@ def countingChild (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : Bool | false => child ψ c H false | true => reduce (ψ ∪ petals ψ c H ∪ negatedHeartUnits H) -private theorem sat_union_iff (ψ χ : ClauseSet V) (x : V → Bool) : - (ψ ∪ χ).Sat x ↔ ψ.Sat x ∧ χ.Sat x := by - constructor - · exact fun h => ⟨fun C hC => h C (Finset.mem_union_left _ hC), - fun C hC => h C (Finset.mem_union_right _ hC)⟩ - · rintro ⟨hψ, hχ⟩ C hC - exact (Finset.mem_union.mp hC).elim (hψ C) (hχ C) - /-- The negated units express exactly the failure of the heart clause. -/ theorem sat_negatedHeartUnits_iff (H : Finset (Literal V)) (x : V → Bool) : (negatedHeartUnits H).Sat x ↔ ¬ ∃ l ∈ H, x l.1 = l.2 := by diff --git a/ComplexityTests/ClauseSetSatisfiable.lean b/ComplexityTests/ClauseSetSatisfiable.lean new file mode 100644 index 000000000..0446de96e --- /dev/null +++ b/ComplexityTests/ClauseSetSatisfiable.lean @@ -0,0 +1,63 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +import Complexity.Logics.Propositional.ClauseSet.Satisfiable + +/-! Tests for satisfiability of clause sets: a satisfiable and an unsatisfiable clause set over two +variables, decided by evaluation; a clause that makes a satisfiable set unsatisfiable; relabelling +along an injective map, which preserves satisfiability, and along a map identifying two variables, +which does not; agreement with `CNF.Satisfiable`; and the width bound under relabelling. -/ + +namespace ComplexityTests.ClauseSetSatisfiable + +open Cslib.Logic.PL + +/-- `(x₀ ∨ x₁) ∧ ¬x₀`, satisfied only by `x₀ = false`, `x₁ = true`. -/ +private def ψ : ClauseSet (Fin 2) := {{(0, true), (1, true)}, {(0, false)}} + +/-- `x₀ ∧ ¬x₀`. -/ +private def φ : ClauseSet (Fin 2) := {{(0, true)}, {(0, false)}} + +example : ψ.Satisfiable := by decide + +example : ¬φ.Satisfiable := by decide + +-- The satisfying assignment, and a non-satisfying one. +example : ψ.Sat (fun i => i == 1) ∧ ¬ψ.Sat fun _ => true := by decide + +-- Adding the clause `¬x₁` leaves no satisfying assignment. +example : ¬(ψ ∪ {{(1, false)}}).Satisfiable := by decide + +-- `sat_insert_iff` splits off the inserted clause: the only satisfying assignment of `ψ` falsifies +-- `¬x₁`. +example : ¬(insert {(1, false)} ψ).Sat fun i => i == 1 := by + simp only [ClauseSet.sat_insert_iff, not_and] + decide + +-- An injective relabelling preserves satisfiability, by the lemma and by evaluation. +example : (ψ.relabel (Fin.succ : Fin 2 → Fin 3)).Satisfiable := + (ClauseSet.satisfiable_relabel (Fin.succ_injective 2) ψ).mpr (by decide) + +example : (ψ.relabel (Fin.succ : Fin 2 → Fin 3)).Satisfiable := by decide + +-- Identifying `x₀` and `x₁` turns `ψ` into `y ∧ ¬y`: injectivity is needed. +example : ¬(ψ.relabel fun _ : Fin 2 => (0 : Fin 1)).Satisfiable := by decide + +-- The assignment `σ` satisfies the relabelled set exactly when `σ ∘ f` satisfies `ψ`. +example : (ψ.relabel (Fin.succ : Fin 2 → Fin 3)).Sat fun i => i != 1 := + (ClauseSet.sat_relabel_iff _ ψ _).mpr (by decide) + +example : ψ.toCNF.Satisfiable := (ClauseSet.satisfiable_toCNF_iff ψ).mpr (by decide) + +example : ¬φ.toCNF.Satisfiable := by + rw [ClauseSet.satisfiable_toCNF_iff] + decide + +-- Relabelling keeps clauses of width at most `2`. +example : ∀ C ∈ ψ.relabel (Fin.succ : Fin 2 → Fin 3), C.card ≤ 2 := + fun _ hC => ClauseSet.card_le_of_mem_relabel (by decide) hC + +end ComplexityTests.ClauseSetSatisfiable From 71e23d7094bfe0ece18ab56ea7fe4680fd51ad62 Mon Sep 17 00:00:00 2001 From: Andras Salamon Date: Sat, 31 Oct 2026 02:21:37 +0000 Subject: [PATCH 2/2] feat(logic): CNF.satisfiable_toClauseSet_iff The converse of ClauseSet.satisfiable_toCNF_iff, with a test. Co-Authored-By: Claude Opus 5.5 --- .../Propositional/ClauseSet/Satisfiable.lean | 18 +++++++++++++----- ComplexityTests/ClauseSetSatisfiable.lean | 5 +++++ 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean b/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean index c8375400a..882c5e40a 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean @@ -14,10 +14,11 @@ public import Complexity.Logics.Propositional.ClauseSet.Basic A clause set is *satisfiable* when some assignment satisfies all of its clauses (`ClauseSet.Satisfiable`). Over a finite type of variables this is decidable, and it agrees with -satisfiability of a formula listing the clauses (`ClauseSet.satisfiable_toCNF_iff`). Satisfaction -of unions, insertions, images and indexed unions of clause sets is characterized clause by clause, -and renaming the variables along an injective map preserves satisfiability -(`ClauseSet.satisfiable_relabel`), as for formulas (`CNF.satisfiable_relabel`). +satisfiability of a formula listing the clauses, and a formula with satisfiability of its clause set +(`ClauseSet.satisfiable_toCNF_iff`, `CNF.satisfiable_toClauseSet_iff`). Satisfaction of unions, +insertions, images and indexed unions of clause sets is characterized clause by clause, and renaming +the variables along an injective map preserves satisfiability (`ClauseSet.satisfiable_relabel`), as +for formulas (`CNF.satisfiable_relabel`). ## Main definitions @@ -26,7 +27,9 @@ and renaming the variables along an injective map preserves satisfiability ## Main results -* `Cslib.Logic.PL.ClauseSet.satisfiable_toCNF_iff`: agreement with `CNF.Satisfiable`. +* `Cslib.Logic.PL.ClauseSet.satisfiable_toCNF_iff`, + `Cslib.Logic.PL.CNF.satisfiable_toClauseSet_iff`: agreement with `CNF.Satisfiable`, in both + directions. * `Cslib.Logic.PL.ClauseSet.sat_union_iff`, `Cslib.Logic.PL.ClauseSet.sat_insert_iff`, `Cslib.Logic.PL.ClauseSet.sat_singleton_iff`, `Cslib.Logic.PL.ClauseSet.sat_empty`, `Cslib.Logic.PL.ClauseSet.sat_image_iff`, `Cslib.Logic.PL.ClauseSet.sat_biUnion_iff`: @@ -60,6 +63,11 @@ instance [Fintype V] [DecidableEq V] (ψ : ClauseSet V) : Decidable ψ.Satisfiab theorem satisfiable_toCNF_iff (ψ : ClauseSet V) : ψ.toCNF.Satisfiable ↔ ψ.Satisfiable := by simp only [CNF.Satisfiable, ClauseSet.eval_toCNF_eq_true_iff, Satisfiable] +/-- A formula is satisfiable exactly when its clause set is. -/ +theorem _root_.Cslib.Logic.PL.CNF.satisfiable_toClauseSet_iff [DecidableEq V] (φ : CNF V) : + φ.toClauseSet.Satisfiable ↔ φ.Satisfiable := + exists_congr fun x => CNF.sat_toClauseSet_iff φ x + /-! ### Satisfaction of combined clause sets -/ section Sat diff --git a/ComplexityTests/ClauseSetSatisfiable.lean b/ComplexityTests/ClauseSetSatisfiable.lean index 0446de96e..6895828f0 100644 --- a/ComplexityTests/ClauseSetSatisfiable.lean +++ b/ComplexityTests/ClauseSetSatisfiable.lean @@ -56,6 +56,11 @@ example : ¬φ.toCNF.Satisfiable := by rw [ClauseSet.satisfiable_toCNF_iff] decide +-- A formula listing the clauses of `φ` is unsatisfiable, and so is its clause set again. +example : ¬φ.toCNF.toClauseSet.Satisfiable := by + rw [CNF.satisfiable_toClauseSet_iff, ClauseSet.satisfiable_toCNF_iff] + decide + -- Relabelling keeps clauses of width at most `2`. example : ∀ C ∈ ψ.relabel (Fin.succ : Fin 2 → Fin 3), C.card ≤ 2 := fun _ hC => ClauseSet.card_le_of_mem_relabel (by decide) hC