1	import Lax434930.PolynomialTime
2
	… module docstring, 9 lines
12
13	namespace Lax429075.CNF
14
15	structure Literal where
16	index : ℕ
17	positive : Bool
18	deriving DecidableEq
19
20	abbrev Clause := List Literal
21	abbrev Formula := List Clause
22	abbrev Assignment := ℕ → Bool
23
24	def Literal.eval (l : Literal) (ρ : Assignment) : Bool :=
25	if l.positive then ρ l.index else !(ρ l.index)
26
27	def eval (F : Formula) (ρ : Assignment) : Bool :=
28	F.all fun C => C.any fun l => l.eval ρ
29
30	def Satisfiable (F : Formula) : Prop := ∃ ρ, eval F ρ = true
31
32	end Lax429075.CNF
33

1	import Lax429075.CNF
2
	… module docstring, 10 lines
13
14	namespace Lax429075.Encoding
15
16	open CNF Lax434930.PolynomialTime
17
18	def encodeList {α : Type} (encode : α → Word) : List α → Word
19	\| [] => [false]
20	\| a :: as => true :: (encode a ++ encodeList encode as)
21
22	def encodeNat (n : ℕ) : Word := List.replicate n true ++ [false]
23
24	def encodeLiteral (l : Literal) : Word := encodeNat l.index ++ [l.positive]
25
26	def encodeClause : Clause → Word := encodeList encodeLiteral
27
28	def encodeCNF : Formula → Word := encodeList encodeClause
29
30	def parseNat : Word → Option (ℕ × Word)
31	\| [] => none
32	\| false :: w => some (0, w)
33	\| true :: w => do
34	let (n, rest) ← parseNat w
35	pure (n + 1, rest)
36
37	def parseLiteral (w : Word) : Option (Literal × Word) := do
38	let (n, rest) ← parseNat w
39	match rest with
40	\| [] => none
41	\| sign :: tail => pure (⟨n, sign⟩, tail)
42
43	def parseList {α : Type} (parse : Word → Option (α × Word)) :
44	ℕ → Word → Option (List α × Word)
45	\| 0, _ => none
46	\| _ + 1, [] => none
47	\| _ + 1, false :: w => some ([], w)
48	\| fuel + 1, true :: w => do
49	let (a, rest) ← parse w
50	let (as, tail) ← parseList parse fuel rest
51	pure (a :: as, tail)
52
53	def parseClause (w : Word) : Option (Clause × Word) := parseList parseLiteral w.length w
54
55	def decodeCNF (w : Word) : Option Formula := do
56	let (F, rest) ← parseList parseClause w.length w
57	if rest = [] then pure F else none
58
59	end Lax429075.Encoding
60

1	import Lax429075.Encoding
2
	… module docstring, 7 lines
10
11	namespace Lax429075.EncodingCorrect
12
13	open CNF Encoding
14
15	axiom roundtrip (F : Formula) : decodeCNF (encodeCNF F) = some F
16
17	end Lax429075.EncodingCorrect
18

1	import Lax429075.Encoding
2	import Lax434930.Certificates
3
	… module docstring, 10 lines
14
15	namespace Lax429075.Satisfiability
16
17	open CNF Encoding Lax434930.PolynomialTime Lax434930.Certificates
18
19	def assignment (y : Word) : Assignment := fun i => (y[i]?).getD false
20
21	def SAT : Language := {w \| ∃ F, encodeCNF F = w ∧ Satisfiable F}
22
23	def Verifier : Language :=
24	{z \| ∃ (F : Formula) (y : Word), z = pair (encodeCNF F) y ∧ eval F (assignment y) = true}
25
26	end Lax429075.Satisfiability
27

1	import Lax429075.Satisfiability
2
	… module docstring, 7 lines
10
11	namespace Lax429075.SATEncoding
12
13	open CNF Encoding Satisfiability
14
15	axiom correct (F : Formula) : encodeCNF F ∈ SAT ↔ Satisfiable F
16
17	end Lax429075.SATEncoding
18

Lax Lean Archive

The Cook–Levin Theorem

1	import Lax429075.CNF
2
	… module docstring, 10 lines
13
14	namespace Lax429075.Circuits
15
16	open CNF
17
18	inductive Gate
19	\| input
20	\| constant (value : Bool)
21	\| neg (a : ℕ)
22	\| conj (a b : ℕ)
23	\| disj (a b : ℕ)
24	deriving DecidableEq
25
26	def Gate.inputs : Gate → List ℕ
27	\| .input \| .constant _ => []
28	\| .neg a => [a]
29	\| .conj a b \| .disj a b => [a, b]
30
31	structure Circuit where
32	gates : List Gate
33	output : Fin gates.length
34	ordered : ∀ g i, (g, i) ∈ gates.zipIdx → ∀ j ∈ g.inputs, j < i
35
36	def Gate.check (ρ : Assignment) (i : ℕ) : Gate → Bool
37	\| .input => true
38	\| .constant b => ρ i == b
39	\| .neg a => ρ i == !(ρ a)
40	\| .conj a b => ρ i == (ρ a && ρ b)
41	\| .disj a b => ρ i == (ρ a \|\| ρ b)
42
43	def check (C : Circuit) (ρ : Assignment) : Bool :=
44	ρ C.output && C.gates.zipIdx.all (fun gi => gi.1.check ρ gi.2)
45
46	def Satisfiable (C : Circuit) : Prop := ∃ ρ, check C ρ = true
47
48	end Lax429075.Circuits
49

1	import Lax429075.Circuits
2
	… module docstring, 9 lines
12
13	namespace Lax429075.Tseitin
14
15	open CNF Circuits
16
17	def positive (i : ℕ) : Literal := ⟨i, true⟩
18	def negative (i : ℕ) : Literal := ⟨i, false⟩
19
20	def gateClauses (i : ℕ) : Gate → Formula
21	\| .input => []
22	\| .constant b => [[⟨i, b⟩]]
23	\| .neg a => [[positive i, positive a], [negative i, negative a]]
24	\| .conj a b => [[negative i, positive a], [negative i, positive b],
25	[positive i, negative a, negative b]]
26	\| .disj a b => [[positive i, negative a], [positive i, negative b],
27	[negative i, positive a, positive b]]
28
29	def encode (C : Circuit) : Formula :=
30	[[positive C.output]] ++ C.gates.zipIdx.flatMap (fun gi => gateClauses gi.2 gi.1)
31
32	end Lax429075.Tseitin
33