Skip to content

Commit 99f4779

Browse files
Marijn HeuleMarijn Heule
Marijn Heule
authored and
Marijn Heule
committed
resolution
1 parent d173bf5 commit 99f4779

File tree

3 files changed

+146
-15
lines changed

3 files changed

+146
-15
lines changed

‎LAMR/Examples/using_sat_solvers/dpll.lean‎

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -4,17 +4,18 @@ import LAMR.Util.Propositional.Syntax
44
/-! A very basic DPLL SAT solver. -/
55

66
def PropAssignment.evalClause (τ : PropAssignment) (c : Clause) : Bool :=
7-
(c : List Lit).foldl (init := false) (fun v l => v ∨ (τ.evalLit? l |>.get!))
7+
(c : List Lit).foldl (init := false) (fun v l => v ∨ τ.evalLit l)
8+
-- (c : List Lit).foldl (init := false) (fun v l => v ∨ (τ.evalLit? l |>.get!))
89

910
def PropAssignment.evalCnf (τ : PropAssignment) (Γ : CnfForm) : Bool :=
1011
(Γ : List Clause).foldl (init := true) (fun v c => v ∧ τ.evalClause c)
1112

1213
/-- Erases all elements equal to the argument from the list. -/
1314
def List.eraseAll {α} [BEq α] : List α → α → List α
14-
| [], _ => []
15-
| a::as, b => match a == b with
16-
| true => List.eraseAll as b
17-
| false => a :: List.eraseAll as b
15+
| [], _ => []
16+
| a :: as, b => match a == b with
17+
| true => List.eraseAll as b
18+
| false => a :: List.eraseAll as b
1819

1920
/-- Simplifies the CNF assuming `x` is true. `x` must not be a constant. -/
2021
-- textbook: simplify
@@ -44,7 +45,7 @@ def CnfForm.findUnit : CnfForm → Option Lit
4445
| [x] :: _ => some x
4546
| _ :: cs => findUnit cs
4647

47-
/-- Performs a round of unit propagation on `φ` under the assignment `τ`.
48+
/-- Performs a round of unit propagation on `Γ` under the assignment `τ`.
4849
Returns an updated assignment and a simplified formula.
4950
5051
Assumes no additions to `τ` since last `simplify _ φ` call.
@@ -106,7 +107,7 @@ where
106107
let (τ', Γ') := propagateWithNew x τ Γ
107108
dpllSatAux τ' Γ'
108109

109-
/-- Solve `φ` using DPLL. Return a satisfying assignment if found, otherwise `none`. -/
110+
/-- Solve `Γ` using DPLL. Return a satisfying assignment if found, otherwise `none`. -/
110111
def dpllSat (Γ : CnfForm) : Option PropAssignment :=
111112
let ⟨τ, Γ⟩ := propagateUnits [] Γ
112113
(dpllSatAux τ Γ).map fun ⟨τ, _⟩ => τ
@@ -128,9 +129,9 @@ def τ := dpllSat Γ |>.get!
128129

129130
end hidden
130131

131-
theorem dpllSatYesSpec : ∀ ϕ, ∀ τ, dpllSat ϕ = some τ ↔ τ.evalCnf ϕ = true := by
132+
theorem dpllSatYesSpec : ∀ Γ, ∀ τ, dpllSat Γ = some τ ↔ τ.evalCnf Γ = true := by
132133
admit -- TODO
133-
theorem dpllSatNoSpec : ∀ ϕ, dpllSat ϕ = none ↔ ∀ (τ : PropAssignment), τ.evalCnf ϕ = false := by
134+
theorem dpllSatNoSpec : ∀ Γ, dpllSat Γ = none ↔ ∀ (τ : PropAssignment), τ.evalCnf Γ = false := by
134135
admit -- TODO
135136

136137
def String.splitOn' (s : String) (sep : String) : List String :=
@@ -151,12 +152,12 @@ def readDimacs (fname : String) : IO CnfForm := do
151152

152153
let mut cnf : CnfForm := []
153154
for ln in lns do
154-
let vars := ln.splitOn' " "
155-
let vars := vars.take (vars.length - 1) -- drop "0"
156-
let vars := vars.map Lit.ofDimacs?
157-
if vars.any (·.isNone) then
155+
let lits := ln.splitOn' " "
156+
let lits := lits.take (lits.length - 1) -- drop "0"
157+
let lits := lits.map Lit.ofDimacs?
158+
if lits.any (·.isNone) then
158159
throw <| IO.userError s!"cannot parse line '{ln}'"
159-
cnf := (vars.map Option.get!) :: cnf
160+
cnf := (lits.map Option.get!) :: cnf
160161

161162
return cnf
162163

‎LAMR/Examples/using_sat_solvers/resolution.lean‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
import LAMR
2+
3+
/-
4+
Resolution proof in Lean
5+
-/
6+
7+
namespace Resolution
8+
9+
/--
10+
The resolution Step.
11+
12+
C ∨ p
13+
D ∨ ¬ p
14+
------- RES
15+
C ∨ D
16+
-/
17+
18+
def resolve (c₁ c₂ : Clause) (var : String) : Clause :=
19+
(c₁.erase (Lit.pos var)).union' (c₂.erase (Lit.neg var))
20+
21+
/--
22+
A line of a resolution proof is either a hypothesis or the result of a
23+
resolution step.
24+
-/
25+
inductive Step where
26+
| hyp (clause : Clause) : Step
27+
| res (var : String) (pos neg : Nat) : Step
28+
deriving Inhabited, Repr
29+
30+
def Proof := Array Step deriving Inhabited, Repr
31+
32+
-- Ignore this: it is boilerplate to make the `p[i]` notation work.
33+
instance : GetElem Proof Nat Step (fun xs i => i < xs.size) :=
34+
inferInstanceAs (GetElem (Array Step) _ _ _)
35+
36+
-- determines whether a proof is well-formed
37+
def Proof.wellFormed (p : Proof) : Bool := Id.run do
38+
for i in [:p.size] do
39+
match p[i]! with
40+
| Step.hyp _ => continue
41+
| Step.res _ pos neg =>
42+
if i ≤ pos ∨ i ≤ neg then
43+
return false
44+
true
45+
46+
-- prints out the proof
47+
def Proof.show (p : Proof) : IO Unit := do
48+
if ¬ p.wellFormed then
49+
IO.println "Proof is not well-formed."
50+
return
51+
let mut clauses : Array Clause := #[]
52+
for i in [:p.size] do
53+
match p[i]! with
54+
| Step.hyp c =>
55+
clauses := clauses.push c
56+
IO.println s!"{i}: hypothesis: {c}"
57+
| Step.res var pos neg =>
58+
let resolvent := resolve clauses[pos]! clauses[neg]! var
59+
clauses := clauses.push resolvent
60+
IO.println s!"{i}: resolve {pos}, {neg} on {var}: {resolvent}"
61+
62+
end Resolution
63+
64+
section
65+
open Resolution
66+
67+
def example0 : Proof := #[
68+
.hyp clause!{-p -q r}, -- 0
69+
.hyp clause!{-r}, -- 1
70+
.hyp clause!{p -q}, -- 2
71+
.hyp clause!{-s q}, -- 3
72+
.hyp clause!{s}, -- 4
73+
.res "r" 0 1, -- 5 -p -q
74+
.res "s" 4 3, -- 6 q
75+
.res "q" 6 2, -- 7 p
76+
.res "p" 7 5, -- 8 -q
77+
.res "q" 6 8 -- 9 ⊥
78+
]
79+
80+
#eval example0.wellFormed
81+
#eval example0.show
82+
83+
def example1 : Proof := #[
84+
.hyp clause!{p q}, -- 0
85+
.hyp clause!{-p}, -- 1
86+
.hyp clause!{-q}, -- 2
87+
.res "p" 0 1, -- 3 q
88+
.res "q" 3 2 -- 4 ⊥
89+
]
90+
91+
#eval example1.wellFormed
92+
#eval example1.show
93+
94+
def example2 : Proof := #[
95+
.hyp clause!{ p q r}, -- 0
96+
.hyp clause!{-p s}, -- 1
97+
.hyp clause!{-q s}, -- 2
98+
.hyp clause!{-r s}, -- 3
99+
.hyp clause!{-s}, -- 4
100+
.res "p" 0 1, -- 5 q r s
101+
.res "q" 5 2, -- 6 r s
102+
.res "r" 6 3, -- 7 s
103+
.res "s" 7 4 -- 8 ⊥
104+
]
105+
106+
#eval example2.wellFormed
107+
#eval example2.show
108+
109+
-- Homework: Finish this to get a proof of ⊥.
110+
def example3 : Proof := #[
111+
.hyp clause!{ p q -r}, -- 0
112+
.hyp clause!{-p -q r}, -- 1
113+
.hyp clause!{ q r -s}, -- 2
114+
.hyp clause!{-q -r s}, -- 3
115+
.hyp clause!{ p r s}, -- 4
116+
.hyp clause!{-p -r -s}, -- 5
117+
.hyp clause!{-p q s}, -- 6
118+
.hyp clause!{ p -q -s} -- 7
119+
]
120+
121+
#eval example3.wellFormed
122+
#eval example3.show
123+
124+
end

‎LAMR/Examples/using_sat_solvers/tseitin.lean‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,13 +91,17 @@ def defsImplToCnf (defs : Array NnfForm) : CnfForm := aux defs.toList 0
9191
where aux : List NnfForm → Nat → CnfForm
9292
| [], _ => []
9393
| nnf :: nnfs, n => implToCnf (lit (defLit n)) nnf ++ aux nnfs (n + 1)
94+
95+
def defsImplToCnf' : List NnfForm → Nat → CnfForm
96+
| [], _ => []
97+
| nnf :: nnfs, n => implToCnf (lit (defLit n)) nnf ++ defsImplToCnf' nnfs (n + 1)
9498
-- end: implToCnf
9599

96100
-- textbook: toCnf
97101
def orToCnf : NnfForm → Clause → Array NnfForm → Clause × Array NnfForm
98102
| lit Lit.tr, _, defs => ([Lit.tr], defs)
99103
| lit Lit.fls, cls, defs => (cls, defs)
100-
| lit l, cls, defs => (l :: cls, defs)
104+
| lit l, cls, defs => (l :: cls, defs)
101105
| disj A B, cls, defs =>
102106
let ⟨cls1, defs1⟩ := orToCnf A cls defs
103107
let ⟨cls2, defs2⟩ := orToCnf B cls1 defs1
@@ -118,13 +122,15 @@ def andToCnf : NnfForm → Array NnfForm → CnfForm × Array NnfForm
118122
def toCnf (A : NnfForm) : CnfForm :=
119123
let ⟨cnf, defs⟩ := andToCnf A #[]
120124
cnf.union' (defsImplToCnf defs)
125+
121126
-- end: toCnf
122127

123128
end hidden
124129

125130
-- textbook: ex1.toCnf
126131
#eval toString ex1.toCnf
127132

133+
128134
/-
129135
Here is ex1:
130136

0 commit comments

Comments
 (0)