-
Notifications
You must be signed in to change notification settings - Fork 1
/
dp.ml
183 lines (146 loc) · 7.15 KB
/
dp.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
(* ========================================================================= *)
(* The Davis-Putnam and Davis-Putnam-Loveland-Logemann procedures. *)
(* *)
(* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* The DP procedure. *)
(* ------------------------------------------------------------------------- *)
let one_literal_rule clauses =
let u = hd (find (fun cl -> length cl = 1) clauses) in
let u' = negate u in
let clauses1 = filter (fun cl -> not (mem u cl)) clauses in
image (fun cl -> subtract cl [u']) clauses1;;
let affirmative_negative_rule clauses =
let neg',pos = partition negative (unions clauses) in
let neg = image negate neg' in
let pos_only = subtract pos neg and neg_only = subtract neg pos in
let pure = union pos_only (image negate neg_only) in
if pure = [] then failwith "affirmative_negative_rule" else
filter (fun cl -> intersect cl pure = []) clauses;;
let resolve_on p clauses =
let p' = negate p and pos,notpos = partition (mem p) clauses in
let neg,other = partition (mem p') notpos in
let pos' = image (filter (fun l -> l <> p)) pos
and neg' = image (filter (fun l -> l <> p')) neg in
let res0 = allpairs union pos' neg' in
union other (filter (non trivial) res0);;
let resolution_blowup cls l =
let m = length(filter (mem l) cls)
and n = length(filter (mem (negate l)) cls) in
m * n - m - n;;
let resolution_rule clauses =
let pvs = filter positive (unions clauses) in
let p = minimize (resolution_blowup clauses) pvs in
resolve_on p clauses;;
(* ------------------------------------------------------------------------- *)
(* Overall procedure. *)
(* ------------------------------------------------------------------------- *)
let rec dp clauses =
if clauses = [] then true else if mem [] clauses then false else
try dp (one_literal_rule clauses) with Failure _ ->
try dp (affirmative_negative_rule clauses) with Failure _ ->
dp(resolution_rule clauses);;
(* ------------------------------------------------------------------------- *)
(* Davis-Putnam satisfiability tester and tautology checker. *)
(* ------------------------------------------------------------------------- *)
let dpsat fm = dp(defcnfs fm);;
let dptaut fm = not(dpsat(Not fm));;
(* ------------------------------------------------------------------------- *)
(* Examples. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
tautology(prime 11);;
dptaut(prime 11);;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* The same thing but with the DPLL procedure. *)
(* ------------------------------------------------------------------------- *)
let posneg_count cls l =
let m = length(filter (mem l) cls)
and n = length(filter (mem (negate l)) cls) in
m + n;;
let rec dpll clauses =
if clauses = [] then true else if mem [] clauses then false else
try dpll(one_literal_rule clauses) with Failure _ ->
try dpll(affirmative_negative_rule clauses) with Failure _ ->
let pvs = filter positive (unions clauses) in
let p = maximize (posneg_count clauses) pvs in
dpll (insert [p] clauses) || dpll (insert [negate p] clauses);;
let dpllsat fm = dpll(defcnfs fm);;
let dplltaut fm = not(dpllsat(Not fm));;
(* ------------------------------------------------------------------------- *)
(* Example. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
dplltaut(prime 11);;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* Iterative implementation with explicit trail instead of recursion. *)
(* ------------------------------------------------------------------------- *)
type trailmix = Guessed | Deduced;;
let unassigned =
let litabs p = match p with Not q -> q | _ -> p in
fun cls trail -> subtract (unions(image (image litabs) cls))
(image (litabs ** fst) trail);;
let rec unit_subpropagate (cls,fn,trail) =
let cls' = map (filter ((not) ** defined fn ** negate)) cls in
let uu = function [c] when not(defined fn c) -> [c] | _ -> failwith "" in
let newunits = unions(mapfilter uu cls') in
if newunits = [] then (cls',fn,trail) else
let trail' = itlist (fun p t -> (p,Deduced)::t) newunits trail
and fn' = itlist (fun u -> (u |-> ())) newunits fn in
unit_subpropagate (cls',fn',trail');;
let unit_propagate (cls,trail) =
let fn = itlist (fun (x,_) -> (x |-> ())) trail undefined in
let cls',fn',trail' = unit_subpropagate (cls,fn,trail) in cls',trail';;
let rec backtrack trail =
match trail with
(p,Deduced)::tt -> backtrack tt
| _ -> trail;;
let rec dpli cls trail =
let cls',trail' = unit_propagate (cls,trail) in
if mem [] cls' then
match backtrack trail with
(p,Guessed)::tt -> dpli cls ((negate p,Deduced)::tt)
| _ -> false
else
match unassigned cls trail' with
[] -> true
| ps -> let p = maximize (posneg_count cls') ps in
dpli cls ((p,Guessed)::trail');;
let dplisat fm = dpli (defcnfs fm) [];;
let dplitaut fm = not(dplisat(Not fm));;
(* ------------------------------------------------------------------------- *)
(* With simple non-chronological backjumping and learning. *)
(* ------------------------------------------------------------------------- *)
let rec backjump cls p trail =
match backtrack trail with
(q,Guessed)::tt ->
let cls',trail' = unit_propagate (cls,(p,Guessed)::tt) in
if mem [] cls' then backjump cls p tt else trail
| _ -> trail;;
let rec dplb cls trail =
let cls',trail' = unit_propagate (cls,trail) in
if mem [] cls' then
match backtrack trail with
(p,Guessed)::tt ->
let trail' = backjump cls p tt in
let declits = filter (fun (_,d) -> d = Guessed) trail' in
let conflict = insert (negate p) (image (negate ** fst) declits) in
dplb (conflict::cls) ((negate p,Deduced)::trail')
| _ -> false
else
match unassigned cls trail' with
[] -> true
| ps -> let p = maximize (posneg_count cls') ps in
dplb cls ((p,Guessed)::trail');;
let dplbsat fm = dplb (defcnfs fm) [];;
let dplbtaut fm = not(dplbsat(Not fm));;
(* ------------------------------------------------------------------------- *)
(* Examples. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
dplitaut(prime 101);;
dplbtaut(prime 101);;
END_INTERACTIVE;;