`XORFamily`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.Isolation
domain: Complexity
line: 10 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.Isolation on GitHub at line 10.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.