IndisputableMonolith.Complexity.SAT.Isolation

   1import Mathlib
   2import IndisputableMonolith.Complexity.SAT.CNF
   3import IndisputableMonolith.Complexity.SAT.XOR
   4
   5namespace IndisputableMonolith
   6namespace Complexity
   7namespace SAT
   8
   9/-- An XOR family for instances of size `n`. -/
  10abbrev XORFamily := (n : Nat) → List (XORSystem n)
  11
  12/-- A system `H` isolates `φ` when `φ ∧ H` has exactly one satisfying assignment. -/
  13def isolates {n} (φ : CNF n) (H : XORSystem n) : Prop :=
  14  UniqueSolutionXOR { φ := φ, H := H }
  15
  16/-- A family `𝓗` is isolating if for every satisfiable `φ`, some `H ∈ 𝓗 n` isolates `φ`. -/
  17def IsolatingFamily (𝓗 : XORFamily) : Prop :=
  18  ∀ {n} (φ : CNF n), Satisfiable φ → ∃ H ∈ 𝓗 n, isolates φ H
  19
  20/-- Deterministic isolation: an explicit, uniformly constructible `𝓗` with polynomial size. -/
  21structure DeterministicIsolation where
  22  𝓗        : XORFamily
  23  polySize : ∃ c k : Nat, ∀ n, (𝓗 n).length ≤ c * n^k
  24  isolates_all : IsolatingFamily 𝓗
  25
  26end SAT
  27end Complexity
  28end IndisputableMonolith
  29