  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.