def
definition
evalLit
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 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25abbrev Assignment (n : Nat) := Var n → Bool
26
27/-- Evaluate a literal under an assignment. -/
28def evalLit {n} (a : Assignment n) : Lit n → Bool
29 | .pos v => a v
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