feat: introduce Std.Sat.CNF

Author: hargoniX

src/Std/Sat.lean

@@ -5,3 +5,4 @@ Authors: Henrik Böving
 -/
 prelude
 import Std.Sat.Basic
+import Std.Sat.CNF

src/Std/Sat/CNF.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Sat.CNF.Basic
+import Std.Sat.CNF.Literal
+import Std.Sat.CNF.Relabel
+import Std.Sat.CNF.RelabelFin

src/Std/Sat/CNF/Basic.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Data.List.Lemmas
+import Std.Sat.CNF.Literal
+
+namespace Std
+namespace Sat
+
+/--
+A clause in a CNF.
+
+The literal `(i, b)` is satisfied is the assignment to `i` agrees with `b`.
+-/
+abbrev CNF.Clause (α : Type u) : Type u := List (Literal α)
+
+/--
+A CNF formula.
+
+Literals are identified by members of `α`.
+-/
+abbrev CNF (α : Type u) : Type u := List (CNF.Clause α)
+
+namespace CNF
+
+/--
+Evaluating a `Clause` with respect to an assignment `f`.
+-/
+def Clause.eval (f : α → Bool) (c : Clause α) : Bool := c.any fun (i, n) => f i == n
+
+@[simp] theorem Clause.eval_nil (f : α → Bool) : Clause.eval f [] = false := rfl
+@[simp] theorem Clause.eval_succ (f : α → Bool) :
+    Clause.eval f (i :: c) = (f i.1 == i.2 || Clause.eval f c) := rfl
+
+/--
+Evaluating a `CNF` formula with respect to an assignment `f`.
+-/
+def eval (f : α → Bool) (g : CNF α) : Bool := g.all fun c => c.eval f
+
+@[simp] theorem eval_nil (f : α → Bool) : eval f [] = true := rfl
+@[simp] theorem eval_succ (f : α → Bool) : eval f (c :: g) = (c.eval f && eval f g) := rfl
+
+@[simp] theorem eval_append (f : α → Bool) (g h : CNF α) :
+    eval f (g ++ h) = (eval f g && eval f h) := List.all_append
+
+instance : HSat α (Clause α) where
+  eval assign clause := Clause.eval assign clause
+
+instance : HSat α (CNF α) where
+  eval assign cnf := eval assign cnf
+
+@[simp] theorem unsat_nil_iff_false : unsatisfiable α ([] : CNF α) ↔ False :=
+  ⟨fun h => by simp [unsatisfiable, (· ⊨ ·)] at h, by simp⟩
+
+@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by
+  simp [(· ⊨ ·)]
+
+@[simp] theorem unsat_nil_cons {g : CNF α} : unsatisfiable α ([] :: g) ↔ True := by
+  simp [unsatisfiable, (· ⊨ ·)]
+
+namespace Clause
+
+/--
+Literal `a` occurs in `Clause` `c`.
+-/
+def mem (a : α) (c : Clause α) : Prop := (a, false) ∈ c ∨ (a, true) ∈ c
+
+instance {a : α} {c : Clause α} [DecidableEq α] : Decidable (mem a c) :=
+  inferInstanceAs <| Decidable (_ ∨ _)
+
+@[simp] theorem not_mem_nil {a : α} : mem a ([] : Clause α) ↔ False := by simp [mem]
+@[simp] theorem mem_cons {a : α} : mem a (i :: c : Clause α) ↔ (a = i.1 ∨ mem a c) := by
+  rcases i with ⟨b, (_|_)⟩
+  · simp [mem, or_assoc]
+  · simp [mem]
+    rw [or_left_comm]
+
+theorem mem_of (h : (a, b) ∈ c) : mem a c := by
+  cases b
+  · left; exact h
+  · right; exact h
+
+theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, mem i c → f i = g i) :
+    eval f c = eval g c := by
+  induction c
+  case nil => rfl
+  case cons i c ih =>
+    simp only [eval_succ]
+    rw [ih, w]
+    · rcases i with ⟨b, (_|_)⟩ <;> simp [mem]
+    · intro j h
+      apply w
+      rcases h with h | h
+      · left
+        apply List.mem_cons_of_mem _ h
+      · right
+        apply List.mem_cons_of_mem _ h
+
+end Clause
+
+/--
+Literal `a` occurs in `CNF` formula `g`.
+-/
+def mem (a : α) (g : CNF α) : Prop := ∃ c, c ∈ g ∧ c.mem a
+
+instance {a : α} {g : CNF α} [DecidableEq α] : Decidable (mem a g) :=
+  inferInstanceAs <| Decidable (∃ _, _)
+
+theorem any_nonEmpty_iff_exists_mem {g : CNF α} :
+    (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, mem a g := by
+  simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, mem,
+    Clause.mem]
+  constructor
+  . intro h
+    rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩
+    rcases hclause2 with ⟨lit, hlit⟩
+    exists lit.fst, clause
+    constructor
+    . assumption
+    . rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all
+  . intro h
+    rcases h with ⟨lit, clause, ⟨hclause1, hclause2⟩⟩
+    exists clause
+    constructor
+    . assumption
+    . cases hclause2 with
+      | inl hl => exact Exists.intro _ hl
+      | inr hr => exact Exists.intro _ hr
+
+@[simp] theorem not_mem_cons : (¬ ∃ a, mem a g) ↔ ∃ n, g = List.replicate n [] := by
+  simp only [← any_nonEmpty_iff_exists_mem]
+  simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false]
+  induction g with
+  | nil =>
+    simp only [List.not_mem_nil, List.isEmpty_iff, false_implies, forall_const, true_iff]
+    exact ⟨0, rfl⟩
+  | cons c g ih =>
+    simp_all [ih, List.isEmpty_iff]
+    constructor
+    · rintro ⟨rfl, n, rfl⟩
+      exact ⟨n+1, rfl⟩
+    · rintro ⟨n, h⟩
+      cases n
+      · simp at h
+      · simp_all only [List.replicate, List.cons.injEq, true_and]
+        exact ⟨_, rfl⟩
+
+instance {g : CNF α} [DecidableEq α] : Decidable (∃ a, mem a g) :=
+  decidable_of_iff (g.any fun c => !c.isEmpty) any_nonEmpty_iff_exists_mem
+
+@[simp] theorem not_mem_nil {a : α} : mem a ([] : CNF α) ↔ False := by simp [mem]
+@[simp] theorem mem_cons {a : α} {i} {c : CNF α} :
+    mem a (i :: c : CNF α) ↔ (Clause.mem a i ∨ mem a c) := by simp [mem]
+
+theorem mem_of (h : c ∈ g) (w : Clause.mem a c) : mem a g := by
+  apply Exists.intro c
+  constructor <;> assumption
+
+@[simp] theorem mem_append {a : α} {x y : CNF α} : mem a (x ++ y) ↔ mem a x ∨ mem a y := by
+  simp [mem, List.mem_append]
+  constructor
+  · rintro ⟨c, (mx | my), mc⟩
+    · left
+      exact ⟨c, mx, mc⟩
+    · right
+      exact ⟨c, my, mc⟩
+  · rintro (⟨c, mx, mc⟩ | ⟨c, my, mc⟩)
+    · exact ⟨c, Or.inl mx, mc⟩
+    · exact ⟨c, Or.inr my, mc⟩
+
+theorem eval_congr (f g : α → Bool) (x : CNF α) (w : ∀ i, mem i x → f i = g i) :
+    eval f x = eval g x := by
+  induction x
+  case nil => rfl
+  case cons c x ih =>
+    simp only [eval_succ]
+    rw [ih, Clause.eval_congr] <;>
+    · intro i h
+      apply w
+      simp [h]
+
+end CNF
+
+end Sat
+end Std

src/Std/Sat/CNF/Literal.lean

@@ -0,0 +1,47 @@
+/-
+Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Josh Clune
+-/
+prelude
+import Init.Data.ToString
+import Std.Sat.Basic
+
+namespace Std
+namespace Sat
+
+/--
+CNF literals identified by some type `α`.
+-/
+abbrev Literal (α : Type u) := α × Bool
+
+namespace Literal
+
+instance [Hashable α] : Hashable (Literal α) where
+  hash := fun x => if x.2 then hash x.1 else hash x.1 + 1
+
+instance : HSat α (Literal α) where
+  eval := fun p l => (p l.1) = l.2
+
+instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := by
+  rw [HSat.eval, instHSat]
+  exact Bool.decEq (p l.fst) l.snd
+
+/--
+Flip the polarity of `l`.
+-/
+def negate (l : Literal α) : Literal α := (l.1, not l.2)
+
+/--
+Output `l` as a DIMACS literal identifier.
+-/
+def dimacs [ToString α] (l : Literal α) : String :=
+  if l.2 then
+    s!"{l.1}"
+  else
+    s!"-{l.1}"
+
+end Literal
+
+end Sat
+end Std

src/Std/Sat/CNF/Relabel.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Std.Sat.CNF.Basic
+
+namespace Std
+namespace Sat
+
+namespace CNF
+
+namespace Clause
+
+/--
+Change the literal type in a `Clause` from `α` to `β` by using `f`.
+-/
+def relabel (f : α → β) (c : Clause α) : Clause β := c.map (fun (i, n) => (f i, n))
+
+@[simp] theorem eval_relabel {f : α → β} {g : β → Bool} {x : Clause α} :
+    (relabel f x).eval g = x.eval (g ∘ f) := by
+  induction x <;> simp_all [relabel]
+
+@[simp] theorem relabel_id' : relabel (id : α → α) = id := by funext; simp [relabel]
+
+theorem relabel_congr {x : Clause α} {f g : α → β} (w : ∀ a, mem a x → f a = g a) :
+    relabel f x = relabel g x := by
+  simp only [relabel]
+  rw [List.map_congr_left]
+  intro ⟨i, b⟩ h
+  congr
+  apply w _ (mem_of h)
+
+-- We need the unapplied equality later.
+@[simp] theorem relabel_relabel' : relabel f ∘ relabel g = relabel (f ∘ g) := by
+  funext i
+  simp only [Function.comp_apply, relabel, List.map_map]
+  rfl
+
+end Clause
+
+/-! ### Relabelling
+
+It is convenient to be able to construct a CNF using a more complicated literal type,
+but eventually we need to embed in `Nat`.
+-/
+
+/--
+Change the literal type in a `CNF` formula from `α` to `β` by using `f`.
+-/
+def relabel (f : α → β) (g : CNF α) : CNF β := g.map (Clause.relabel f)
+
+@[simp] theorem eval_relabel (f : α → β) (g : β → Bool) (x : CNF α) :
+    (relabel f x).eval g = x.eval (g ∘ f) := by
+  induction x <;> simp_all [relabel]
+
+@[simp] theorem relabel_append : relabel f (g ++ h) = relabel f g ++ relabel f h :=
+  List.map_append _ _ _
+
+@[simp] theorem relabel_relabel : relabel f (relabel g x) = relabel (f ∘ g) x := by
+  simp only [relabel, List.map_map, Clause.relabel_relabel']
+
+@[simp] theorem relabel_id : relabel id x = x := by simp [relabel]
+
+theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, mem a x → f a = g a) :
+    relabel f x = relabel g x := by
+  dsimp only [relabel]
+  rw [List.map_congr_left]
+  intro c h
+  apply Clause.relabel_congr
+  intro a m
+  exact w _ (mem_of h m)
+
+theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by
+  simp_all [(· ⊨ ·)]
+
+theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsatisfiable α x)
+    : unsatisfiable β (relabel f x) := by
+  simp_all [unsatisfiable, (· ⊨ ·)]
+
+theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by
+  induction x with
+  | nil => exact Or.inr ⟨0, rfl⟩
+  | cons c x ih => match c with
+    | [] => cases ih with
+      | inl h => left; exact h
+      | inr h =>
+        obtain ⟨n, rfl⟩ := h
+        right
+        exact ⟨n + 1, rfl⟩
+    | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩
+
+theorem unsat_relabel_iff {x : CNF α} {f : α → β}
+    (w : ∀ {a b}, mem a x → mem b x → f a = f b → a = b) :
+    unsatisfiable β (relabel f x) ↔ unsatisfiable α x := by
+  rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)
+  · refine ⟨fun h => ?_, unsat_relabel f⟩
+    have em := Classical.propDecidable
+    let g : β → α := fun b =>
+      if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀
+    have h' := unsat_relabel g h
+    suffices w : relabel g (relabel f x) = x by
+      rwa [w] at h'
+    have : ∀ a, mem a x → g (f a) = a := by
+      intro a h
+      dsimp [g]
+      rw [dif_pos ⟨a, h, rfl⟩]
+      apply w _ h
+      · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).2
+      · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1
+    rw [relabel_relabel, relabel_congr, relabel_id]
+    exact this
+  · cases n <;> simp [unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ]
+
+end CNF
+
+end Sat
+end Std