def
definition
evalClause
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Complexity.SAT.CNF on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
30 | .neg v => ! (a v)
31
32/-- Evaluate a clause (OR over its literals). Empty clause = false. -/
33def evalClause {n} (a : Assignment n) (C : Clause n) : Bool :=
34 C.any (fun l => evalLit a l)
35
36/-- Evaluate a CNF (AND over its clauses). Empty CNF = true. -/
37def evalCNF {n} (a : Assignment n) (φ : CNF n) : Bool :=
38 φ.clauses.all (fun C => evalClause a C)
39
40/-- Satisfiable CNF. -/
41def Satisfiable {n} (φ : CNF n) : Prop :=
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