`BackpropSucceeds`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.Backprop
domain: Complexity
line: 455 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.Backprop on GitHub at line 455.

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

 452  | wire_prop => exact hv
 453
 454/-- Backpropagation succeeds if every legal start reaches a complete consistent state. -/
 455def BackpropSucceeds {n} (φ : CNF n) (H : XORSystem n) : Prop :=
 456  ∀ (_s0 : BPState n),
 457    ∃ s, complete s ∧ consistent s φ H
 458
 459end SAT
 460end Complexity
 461end IndisputableMonolith

papers checked against this theorem

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