|
1 (* ========================================================================= *) |
|
2 (* THE WAITING SET OF CLAUSES *) |
|
3 (* Copyright (c) 2002-2007 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure Waiting :> Waiting = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* Chatting. *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 val module = "Waiting"; |
|
16 fun chatting l = tracing {module = module, level = l}; |
|
17 fun chat s = (trace s; true); |
|
18 |
|
19 (* ------------------------------------------------------------------------- *) |
|
20 (* A type of waiting sets of clauses. *) |
|
21 (* ------------------------------------------------------------------------- *) |
|
22 |
|
23 type parameters = |
|
24 {symbolsWeight : real, |
|
25 literalsWeight : real, |
|
26 modelsWeight : real, |
|
27 modelChecks : int, |
|
28 models : Model.parameters list}; |
|
29 |
|
30 type distance = real; |
|
31 |
|
32 type weight = real; |
|
33 |
|
34 datatype waiting = |
|
35 Waiting of |
|
36 {parameters : parameters, |
|
37 clauses : (weight * (distance * Clause.clause)) Heap.heap, |
|
38 models : Model.model list}; |
|
39 |
|
40 (* ------------------------------------------------------------------------- *) |
|
41 (* Basic operations. *) |
|
42 (* ------------------------------------------------------------------------- *) |
|
43 |
|
44 val default : parameters = |
|
45 {symbolsWeight = 1.0, |
|
46 literalsWeight = 0.0, |
|
47 modelsWeight = 0.0, |
|
48 modelChecks = 20, |
|
49 models = []}; |
|
50 |
|
51 fun size (Waiting {clauses,...}) = Heap.size clauses; |
|
52 |
|
53 val pp = |
|
54 Parser.ppMap |
|
55 (fn w => "Waiting{" ^ Int.toString (size w) ^ "}") |
|
56 Parser.ppString; |
|
57 |
|
58 (*DEBUG |
|
59 val pp = |
|
60 Parser.ppMap |
|
61 (fn Waiting {clauses,...} => |
|
62 map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) |
|
63 (Parser.ppList (Parser.ppTriple Parser.ppReal Parser.ppInt Clause.pp)); |
|
64 *) |
|
65 |
|
66 (* ------------------------------------------------------------------------- *) |
|
67 (* Clause weights. *) |
|
68 (* ------------------------------------------------------------------------- *) |
|
69 |
|
70 local |
|
71 fun clauseSymbols cl = Real.fromInt (LiteralSet.typedSymbols cl); |
|
72 |
|
73 fun clauseLiterals cl = Real.fromInt (LiteralSet.size cl); |
|
74 |
|
75 fun clauseSat modelChecks models cl = |
|
76 let |
|
77 fun g {T,F} = (Real.fromInt T / Real.fromInt (T + F)) + 1.0 |
|
78 fun f (m,z) = g (Model.checkClause {maxChecks = modelChecks} m cl) * z |
|
79 in |
|
80 foldl f 1.0 models |
|
81 end; |
|
82 |
|
83 fun priority cl = 1e~12 * Real.fromInt (Clause.id cl); |
|
84 in |
|
85 fun clauseWeight (parm : parameters) models dist cl = |
|
86 let |
|
87 (*TRACE3 |
|
88 val () = Parser.ppTrace Clause.pp "Waiting.clauseWeight: cl" cl |
|
89 *) |
|
90 val {symbolsWeight,literalsWeight,modelsWeight,modelChecks,...} = parm |
|
91 val lits = Clause.literals cl |
|
92 val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight) |
|
93 val literalsW = Math.pow (clauseLiterals lits, literalsWeight) |
|
94 val modelsW = Math.pow (clauseSat modelChecks models lits, modelsWeight) |
|
95 (*TRACE4 |
|
96 val () = trace ("Waiting.clauseWeight: dist = " ^ |
|
97 Real.toString dist ^ "\n") |
|
98 val () = trace ("Waiting.clauseWeight: symbolsW = " ^ |
|
99 Real.toString symbolsW ^ "\n") |
|
100 val () = trace ("Waiting.clauseWeight: literalsW = " ^ |
|
101 Real.toString literalsW ^ "\n") |
|
102 val () = trace ("Waiting.clauseWeight: modelsW = " ^ |
|
103 Real.toString modelsW ^ "\n") |
|
104 *) |
|
105 val weight = dist * symbolsW * literalsW * modelsW + priority cl |
|
106 (*TRACE3 |
|
107 val () = trace ("Waiting.clauseWeight: weight = " ^ |
|
108 Real.toString weight ^ "\n") |
|
109 *) |
|
110 in |
|
111 weight |
|
112 end; |
|
113 end; |
|
114 |
|
115 (* ------------------------------------------------------------------------- *) |
|
116 (* Adding new clauses. *) |
|
117 (* ------------------------------------------------------------------------- *) |
|
118 |
|
119 fun add waiting (_,[]) = waiting |
|
120 | add waiting (dist,cls) = |
|
121 let |
|
122 (*TRACE3 |
|
123 val () = Parser.ppTrace pp "Waiting.add: waiting" waiting |
|
124 val () = Parser.ppTrace (Parser.ppList Clause.pp) "Waiting.add: cls" cls |
|
125 *) |
|
126 |
|
127 val Waiting {parameters,clauses,models} = waiting |
|
128 |
|
129 val dist = dist + Math.ln (Real.fromInt (length cls)) |
|
130 |
|
131 val weight = clauseWeight parameters models dist |
|
132 |
|
133 fun f (cl,acc) = Heap.add acc (weight cl, (dist,cl)) |
|
134 |
|
135 val clauses = foldl f clauses cls |
|
136 |
|
137 val waiting = |
|
138 Waiting {parameters = parameters, clauses = clauses, models = models} |
|
139 |
|
140 (*TRACE3 |
|
141 val () = Parser.ppTrace pp "Waiting.add: waiting" waiting |
|
142 *) |
|
143 in |
|
144 waiting |
|
145 end; |
|
146 |
|
147 local |
|
148 fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2); |
|
149 |
|
150 fun empty parameters = |
|
151 let |
|
152 val clauses = Heap.new cmp |
|
153 and models = map Model.new (#models parameters) |
|
154 in |
|
155 Waiting {parameters = parameters, clauses = clauses, models = models} |
|
156 end; |
|
157 in |
|
158 fun new parameters cls = add (empty parameters) (0.0,cls); |
|
159 end; |
|
160 |
|
161 (* ------------------------------------------------------------------------- *) |
|
162 (* Removing the lightest clause. *) |
|
163 (* ------------------------------------------------------------------------- *) |
|
164 |
|
165 fun remove (Waiting {parameters,clauses,models}) = |
|
166 if Heap.null clauses then NONE |
|
167 else |
|
168 let |
|
169 val ((_,dcl),clauses) = Heap.remove clauses |
|
170 val waiting = |
|
171 Waiting |
|
172 {parameters = parameters, clauses = clauses, models = models} |
|
173 in |
|
174 SOME (dcl,waiting) |
|
175 end; |
|
176 |
|
177 end |