feat(logic): satisfiability of clause sets

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

Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean

@@ -0,0 +1,162 @@
+/-
+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, 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
+
+* `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`,
+  `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`:
+  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]
+
+/-- 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
+
+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

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

ComplexityTests/ClauseSetSatisfiable.lean

@@ -0,0 +1,68 @@
+/-
+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
+
+-- 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
+
+end ComplexityTests.ClauseSetSatisfiable