polynomial_time_3sat_algorithm

formal source

 182    (∀ φ, Satisfiable φ → ∃ x, alg φ = some x ∧ evalCNF x φ = true) ∧
 183    (∀ φ, ¬Satisfiable φ → alg φ = none)
 184
 185theorem polynomial_time_3sat_algorithm (n : Nat)
 186    (h : polynomial_time_3sat_algorithm_hypothesis n) :
 187    ProgramTarget n →
 188    ∃ (alg : CNF n → Option (Assignment n)),
 189      (∀ φ, Satisfiable φ → ∃ x, alg φ = some x ∧ evalCNF x φ = true) ∧
 190      (∀ φ, ¬Satisfiable φ → alg φ = none) :=
 191  h
 192
 193/-- Backpropagation succeeds when there is a unique solution under XOR constraints.
 194This is a semantic existence result that does not rely on a specific step system. -/
 195theorem backprop_succeeds_of_unique {n} (φ : CNF n) (H : XORSystem n)
 196    (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
 197    BackpropSucceeds φ H := by
 198  intro s0
 199  rcases huniq with ⟨x, hx, _uniq⟩
 200  refine ⟨completeStateFrom x, ?hcomp, ?hcons⟩
 201  · exact complete_completeStateFrom x
 202  · rcases hx with ⟨hxφ, hxH⟩
 203    exact consistent_completeStateFrom x φ H hxφ hxH
 204
 205/-- PC ⇒ backpropagation succeeds (via uniqueness).
 206Note: with the current abstract step semantics, uniqueness alone suffices for success.
 207PC becomes relevant once a concrete BPStep is connected to semantic forcing. -/
 208theorem backprop_succeeds_from_PC {n}
 209    (inputs : Finset (Var n)) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n)
 210    (_hpc : PC inputs aRef φ H)
 211    (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
 212    BackpropSucceeds φ H :=
 213  backprop_succeeds_of_unique φ H huniq
 214
 215end SAT