import HardnessReductions.Logic.Sat

/-!
# Maximum satisfiability

A *counting* predicate. Where a subset problem asks whether a set exists — a
satisfying assignment, a clique, a cover of size `k` —
MAX SAT asks how many clauses an assignment satisfies, and whether that number
reaches a threshold: `CNF.numSat` is a `List.countP`, and the question is an
inequality about it.

The instance type gains a threshold field, so this is a genuinely new shape
rather than a new question about `SatInstance` — which is why the family gets
its own encoding (`MaxSat/Encoding.lean`) rather than sharing `Logic/Sat`'s.

## What the counting costs

Counting is not free in the way exhibiting is. A satisfiability predicate is
invariant under anything that preserves *some* satisfying assignment; a count is
invariant only under maps that preserve clauses one for one. So each transport
lemma of `Logic/Sat.lean` needs its counting twin, proved here:

* `CNF.numSat_congr` — the count depends on the assignment only at the variables
  that occur, so an assignment may be rebuilt anywhere else;
* `CNF.numSat_relabel` — relabeling is a `map` on the clause list, so the count
  is literally the same `countP` read through the labelling;
* `CNF.maxSatAtLeast_relabel_of_injOn` — the two together, in the `Set.InjOn`
  form the representation theorem needs.

The catalog entry is the width-two restriction, `MAX_2SAT` (Garey–Johnson
[LO5]); unrestricted `MAX_SAT` is here only as the problem it restricts, since
the appendix gives it no entry of its own. Hardness of MAX 2SAT: from 3SAT
(`MaxSat/FromSat3.lean`).
-/

namespace Hardness

variable {V W : Type*}

/-! ## Counting satisfied clauses -/

/-- How many clauses of `φ` an assignment satisfies. -/
def CNF.numSat (σ : V → Bool) (φ : CNF V) : ℕ :=
  φ.countP fun c ↦ decide (c.Sat σ)

/-- Meeting the threshold: some assignment satisfies at least `k` clauses. -/
def CNF.MaxSatAtLeast (φ : CNF V) (k : ℕ) : Prop :=
  ∃ σ : V → Bool, k ≤ φ.numSat σ

/-- The count never exceeds the number of clauses. -/
theorem CNF.numSat_le (σ : V → Bool) (φ : CNF V) : φ.numSat σ ≤ φ.length :=
  List.countP_le_length

/-- The count of a concatenation splits. -/
theorem CNF.numSat_append (σ : V → Bool) (φ ψ : CNF V) :
    (φ ++ ψ).numSat σ = φ.numSat σ + ψ.numSat σ :=
  List.countP_append ..

/-- **The count sees only the occurring variables**: two assignments agreeing on
`φ.vars` satisfy the same number of clauses. The counting twin of
`Clause.sat_congr`, and what lets a satisfying assignment be extended to fresh
variables without disturbing the count. -/
theorem CNF.numSat_congr {φ : CNF V} {σ σ' : V → Bool} (h : ∀ v ∈ φ.vars, σ v = σ' v) :
    φ.numSat σ = φ.numSat σ' := by
  refine List.countP_congr fun c hc ↦ ?_
  simp only [decide_eq_true_eq]
  exact Clause.sat_congr fun l hl ↦ h l.var (CNF.mem_vars hc hl)

/-- **Relabeling preserves the count on the nose**: a relabeled formula is a
`map` of the clause list, so counting it under `τ` is counting the original
under `τ ∘ f`. No injectivity is needed — the clauses correspond one for one
however the labels collide. -/
theorem CNF.numSat_relabel (f : V → W) (φ : CNF V) (τ : W → Bool) :
    (φ.relabel f).numSat τ = φ.numSat fun v ↦ τ (f v) := by
  rw [CNF.numSat, CNF.numSat, CNF.relabel, List.countP_map]
  refine List.countP_congr fun c _ ↦ ?_
  simp only [Function.comp_apply, decide_eq_true_eq]
  exact Clause.sat_map_relabel c

/-- Relabeling preserves and reflects the threshold as soon as the map is
injective *on the variables that occur* — the counting twin of
`CNF.satisfiable_relabel_of_injOn`, and the form the representation theorem
needs. Reflection is free; preservation transports the assignment along `f` and
then appeals to `CNF.numSat_congr`, the count being blind to the labels no
occurring variable carries. -/
theorem CNF.maxSatAtLeast_relabel_of_injOn {f : V → W} {φ : CNF V}
    (hf : Set.InjOn f φ.vars) (k : ℕ) :
    (φ.relabel f).MaxSatAtLeast k ↔ φ.MaxSatAtLeast k := by
  constructor
  · rintro ⟨τ, hτ⟩
    exact ⟨fun v ↦ τ (f v), by rwa [CNF.numSat_relabel] at hτ⟩
  · rintro ⟨σ, hσ⟩
    obtain ⟨τ, hτ⟩ := CNF.exists_relabel_assignment hf σ
    exact ⟨τ, by rwa [CNF.numSat_relabel, CNF.numSat_congr hτ]⟩

/-! ## The problems -/

/-- An instance of a maximum-satisfiability problem: a formula together with the
number of clauses to be satisfied. -/
structure SatThresholdInstance : Type 1 where
  /-- The variable type. -/
  V : Type
  [decEqV : DecidableEq V]
  /-- The formula. -/
  φ : CNF V
  /-- The number of clauses to satisfy. -/
  k : ℕ

attribute [instance] SatThresholdInstance.decEqV

/-- Forget the threshold: the underlying satisfiability instance, which is what
the encoding and the labelling are defined on. -/
def SatThresholdInstance.toSat (x : SatThresholdInstance) : SatInstance :=
  { V := x.V, φ := x.φ }

/-- MAX SAT: can some assignment satisfy `k` of the clauses? Not a catalog entry
of its own — Garey–Johnson give one only to the width-two restriction — but the
problem `MAX_2SAT` restricts. -/
def MAX_SAT : Problem SatThresholdInstance := fun x ↦ x.φ.MaxSatAtLeast x.k

/-- **MAX 2SAT** [LO5]: MAX SAT restricted to clauses of at most two literals,
in the promise-free formulation of `Problem.restrict` — an instance with a wide
clause is simply a no-instance.

The width bound is what makes the problem hard rather than trivial in the
opposite direction: deciding whether *all* clauses of a 2CNF can be satisfied is
2SAT, which is easy, so the counting is doing all the work.

Hardness proof (in `MaxSat/`): from 3SAT (`FromSat3.lean`, ten clauses per
source clause; certified in `FromSat3/Code.lean` and `FromSat3/Adequacy.lean`). -/
def MAX_2SAT : Problem SatThresholdInstance :=
  MAX_SAT.restrict fun x ↦ ∀ c ∈ x.φ, c.length ≤ 2

end Hardness