247structure RSATSeparation where 248 /-- SAT is solvable in O(n) recognition steps for satisfiable instances -/ 249 sat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT → 250 ∃ steps : ℕ, steps ≤ n ∧ ∃ a : Assignment n, satJCost f a = 0 251 /-- No local certifier works for all formulas (adversarial failure) -/ 252 local_certifier_fails : ∀ n : ℕ, ∀ M : Finset (Fin n), 253 M.card < n → 254 ∃ b : Bool, ∃ R : Fin n → Bool, 255 ∃ g : ({i // i ∈ M} → Bool) → Bool, 256 g (BalancedParityHidden.restrict (BalancedParityHidden.enc b R) M) ≠ b 257 /-- UNSAT instances have a persistent topological obstruction -/ 258 unsat_obstruction : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT → 259 ∀ a : Assignment n, satJCost f a ≥ 1 260
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.