pith. machine review for the scientific record. sign in
def

UniqueSolution

definition
show as:
view math explainer →
module
IndisputableMonolith.Complexity.SAT.CNF
domain
Complexity
line
45 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.CNF on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  42  ∃ a : Assignment n, evalCNF a φ = true
  43
  44/-- Uniquely satisfiable CNF. -/
  45def UniqueSolution {n} (φ : CNF n) : Prop :=
  46  ∃! (a : Assignment n), evalCNF a φ = true
  47
  48end SAT
  49end Complexity
  50end IndisputableMonolith

papers checked against this theorem

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