174 (* ------------------------------------------------------------------------- *) |
174 (* ------------------------------------------------------------------------- *) |
175 (* defcnf: computes the definitional conjunctive normal form of a formula *) |
175 (* defcnf: computes the definitional conjunctive normal form of a formula *) |
176 (* 'fm' of propositional logic, introducing auxiliary variables if *) |
176 (* 'fm' of propositional logic, introducing auxiliary variables if *) |
177 (* necessary to avoid an exponential blowup of the formula. The result *) |
177 (* necessary to avoid an exponential blowup of the formula. The result *) |
178 (* formula is satisfiable if and only if 'fm' is satisfiable. *) |
178 (* formula is satisfiable if and only if 'fm' is satisfiable. *) |
|
179 (* Auxiliary variables are introduced as switches for OR-nodes, based *) |
|
180 (* on the observation that "fm1 OR (fm21 AND fm22)" is equisatisfiable *) |
|
181 (* with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR aux)". *) |
179 (* ------------------------------------------------------------------------- *) |
182 (* ------------------------------------------------------------------------- *) |
180 |
183 |
181 (* prop_formula -> prop_formula *) |
184 (* prop_formula -> prop_formula *) |
182 |
185 |
183 fun defcnf fm = |
186 fun defcnf fm = |
184 let |
187 let |
185 (* prop_formula * int -> prop_formula * int *) |
188 (* convert formula to NNF first *) |
|
189 val fm' = nnf fm |
186 (* 'new' specifies the next index that is available to introduce an auxiliary variable *) |
190 (* 'new' specifies the next index that is available to introduce an auxiliary variable *) |
|
191 (* int ref *) |
|
192 val new = ref (maxidx fm' + 1) |
|
193 (* unit -> int *) |
|
194 fun new_idx () = let val idx = !new in new := idx+1; idx end |
|
195 (* prop_formula -> prop_formula *) |
187 fun |
196 fun |
188 (* constants *) |
197 (* constants *) |
189 defcnf_from_nnf (True, new) = (True, new) |
198 defcnf_from_nnf True = True |
190 | defcnf_from_nnf (False, new) = (False, new) |
199 | defcnf_from_nnf False = False |
191 (* literals *) |
200 (* literals *) |
192 | defcnf_from_nnf (BoolVar i, new) = (BoolVar i, new) |
201 | defcnf_from_nnf (BoolVar i) = BoolVar i |
193 | defcnf_from_nnf (Not fm1, new) = (Not fm1, new) (* 'fm1' must be a variable since the formula is in NNF *) |
202 | defcnf_from_nnf (Not fm1) = Not fm1 (* 'fm1' must be a variable since the formula is in NNF *) |
194 (* pushing 'or' inside of 'and' using auxiliary variables *) |
203 (* pushing 'or' inside of 'and' using auxiliary variables *) |
195 | defcnf_from_nnf (Or (fm1, fm2), new) = |
204 | defcnf_from_nnf (Or (fm1, fm2)) = |
196 let |
205 let |
197 val (fm1', new') = defcnf_from_nnf (fm1, new) |
206 val fm1' = defcnf_from_nnf fm1 |
198 val (fm2', new'') = defcnf_from_nnf (fm2, new') |
207 val fm2' = defcnf_from_nnf fm2 |
199 (* prop_formula * prop_formula -> int -> prop_formula * int *) |
208 (* prop_formula * prop_formula -> prop_formula *) |
200 fun defcnf_or (And (fm11, fm12), fm2) new = |
209 fun defcnf_or (And (fm11, fm12), fm2) = |
201 (case fm2 of |
210 (case fm2 of |
202 (* do not introduce an auxiliary variable for literals *) |
211 (* do not introduce an auxiliary variable for literals *) |
203 BoolVar _ => |
212 BoolVar _ => |
204 let |
213 And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2)) |
205 val (fm_a, new') = defcnf_or (fm11, fm2) new |
|
206 val (fm_b, new'') = defcnf_or (fm12, fm2) new' |
|
207 in |
|
208 (And (fm_a, fm_b), new'') |
|
209 end |
|
210 | Not _ => |
214 | Not _ => |
211 let |
215 And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2)) |
212 val (fm_a, new') = defcnf_or (fm11, fm2) new |
|
213 val (fm_b, new'') = defcnf_or (fm12, fm2) new' |
|
214 in |
|
215 (And (fm_a, fm_b), new'') |
|
216 end |
|
217 | _ => |
216 | _ => |
218 let |
217 let |
219 val aux = BoolVar new |
218 val aux = BoolVar (new_idx ()) |
220 val (fm_a, new') = defcnf_or (fm11, aux) (new+1) |
|
221 val (fm_b, new'') = defcnf_or (fm12, aux) new' |
|
222 val (fm_c, new''') = defcnf_or (fm2, Not aux) new'' |
|
223 in |
219 in |
224 (And (And (fm_a, fm_b), fm_c), new''') |
220 And (And (defcnf_or (fm11, aux), defcnf_or (fm12, aux)), defcnf_or (fm2, Not aux)) |
225 end) |
221 end) |
226 | defcnf_or (fm1, And (fm21, fm22)) new = |
222 | defcnf_or (fm1, And (fm21, fm22)) = |
227 (case fm1 of |
223 (case fm1 of |
228 (* do not introduce an auxiliary variable for literals *) |
224 (* do not introduce an auxiliary variable for literals *) |
229 BoolVar _ => |
225 BoolVar _ => |
230 let |
226 And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22)) |
231 val (fm_a, new') = defcnf_or (fm1, fm21) new |
|
232 val (fm_b, new'') = defcnf_or (fm1, fm22) new' |
|
233 in |
|
234 (And (fm_a, fm_b), new'') |
|
235 end |
|
236 | Not _ => |
227 | Not _ => |
237 let |
228 And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22)) |
238 val (fm_a, new') = defcnf_or (fm1, fm21) new |
|
239 val (fm_b, new'') = defcnf_or (fm1, fm22) new' |
|
240 in |
|
241 (And (fm_a, fm_b), new'') |
|
242 end |
|
243 | _ => |
229 | _ => |
244 let |
230 let |
245 val aux = BoolVar new |
231 val aux = BoolVar (new_idx ()) |
246 val (fm_a, new') = defcnf_or (fm1, Not aux) (new+1) |
|
247 val (fm_b, new'') = defcnf_or (fm21, aux) new' |
|
248 val (fm_c, new''') = defcnf_or (fm22, aux) new'' |
|
249 in |
232 in |
250 (And (fm_a, And (fm_b, fm_c)), new''') |
233 And (defcnf_or (fm1, Not aux), And (defcnf_or (fm21, aux), defcnf_or (fm22, aux))) |
251 end) |
234 end) |
252 (* neither subformula contains 'and' *) |
235 (* neither subformula contains 'and' *) |
253 | defcnf_or (fm1, fm2) new = |
236 | defcnf_or (fm1, fm2) = |
254 (Or (fm1, fm2), new) |
237 Or (fm1, fm2) |
255 in |
238 in |
256 defcnf_or (fm1', fm2') new'' |
239 defcnf_or (fm1', fm2') |
257 end |
240 end |
258 (* 'and' as outermost connective is left untouched *) |
241 (* 'and' as outermost connective is left untouched *) |
259 | defcnf_from_nnf (And (fm1, fm2), new) = |
242 | defcnf_from_nnf (And (fm1, fm2)) = |
260 let |
243 And (defcnf_from_nnf fm1, defcnf_from_nnf fm2) |
261 val (fm1', new') = defcnf_from_nnf (fm1, new) |
|
262 val (fm2', new'') = defcnf_from_nnf (fm2, new') |
|
263 in |
|
264 (And (fm1', fm2'), new'') |
|
265 end |
|
266 val fm' = nnf fm |
|
267 in |
244 in |
268 (fst o defcnf_from_nnf) (fm', (maxidx fm')+1) |
245 defcnf_from_nnf fm' |
269 end; |
246 end; |
270 |
247 |
271 (* ------------------------------------------------------------------------- *) |
248 (* ------------------------------------------------------------------------- *) |
272 (* exists: computes the disjunction over a list 'xs' of propositional *) |
249 (* exists: computes the disjunction over a list 'xs' of propositional *) |
273 (* formulas *) |
250 (* formulas *) |