src/HOL/ex/SAT_Examples.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 42012 2c3fe3cbebae child 47432 e1576d13e933 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (*  Title:      HOL/ex/SAT_Examples.thy
2     Author:     Alwen Tiu, Tjark Weber
4 *)
6 header {* Examples for the 'sat' and 'satx' tactic *}
8 theory SAT_Examples imports Main
9 begin
11 (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
12 (* ML {* sat.solver := "minisat_with_proofs"; *} *)
13 ML {* sat.trace_sat := true; *}
14 ML {* quick_and_dirty := true; *}
16 lemma "True"
17 by sat
19 lemma "a | ~a"
20 by sat
22 lemma "(a | b) & ~a \<Longrightarrow> b"
23 by sat
25 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
26 (*
27 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
28 *)
29 by sat
31 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
32 (*
33 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
34 apply (erule exE | erule conjE)+
35 *)
36 by satx
38 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
39   \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
40 (*
41 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
42 *)
43 by sat
45 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
46   \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
47 (*
48 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
49 apply (erule exE | erule conjE)+
50 *)
51 by satx
53 lemma "P=P=P=P=P=P=P=P=P=P"
54 by sat
56 lemma "P=P=P=P=P=P=P=P=P=P"
57 by satx
59 lemma  "!! a b c. [| a | b | c | d ;
60 e | f | (a & d) ;
61 ~(a | (c & ~c)) | b ;
62 ~(b & (x | ~x)) | c ;
63 ~(d | False) | c ;
64 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
65 by sat
67 lemma  "!! a b c. [| a | b | c | d ;
68 e | f | (a & d) ;
69 ~(a | (c & ~c)) | b ;
70 ~(b & (x | ~x)) | c ;
71 ~(d | False) | c ;
72 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
73 by satx
75 text {* eta-Equivalence *}
77 lemma "(ALL x. P x) | ~ All P"
78 by sat
80 ML {* sat.trace_sat := false; *}
81 ML {* quick_and_dirty := false; *}
83 method_setup rawsat =
84   {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
85   "SAT solver (no preprocessing)"
87 (* ML {* Toplevel.profiling := 1; *} *)
89 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
91 lemma assumes 1: "~x0"
92 and 2: "~x30"
93 and 3: "~x29"
94 and 4: "~x59"
95 and 5: "x1 | x31 | x0"
96 and 6: "x2 | x32 | x1"
97 and 7: "x3 | x33 | x2"
98 and 8: "x4 | x34 | x3"
99 and 9: "x35 | x4"
100 and 10: "x5 | x36 | x30"
101 and 11: "x6 | x37 | x5 | x31"
102 and 12: "x7 | x38 | x6 | x32"
103 and 13: "x8 | x39 | x7 | x33"
104 and 14: "x9 | x40 | x8 | x34"
105 and 15: "x41 | x9 | x35"
106 and 16: "x10 | x42 | x36"
107 and 17: "x11 | x43 | x10 | x37"
108 and 18: "x12 | x44 | x11 | x38"
109 and 19: "x13 | x45 | x12 | x39"
110 and 20: "x14 | x46 | x13 | x40"
111 and 21: "x47 | x14 | x41"
112 and 22: "x15 | x48 | x42"
113 and 23: "x16 | x49 | x15 | x43"
114 and 24: "x17 | x50 | x16 | x44"
115 and 25: "x18 | x51 | x17 | x45"
116 and 26: "x19 | x52 | x18 | x46"
117 and 27: "x53 | x19 | x47"
118 and 28: "x20 | x54 | x48"
119 and 29: "x21 | x55 | x20 | x49"
120 and 30: "x22 | x56 | x21 | x50"
121 and 31: "x23 | x57 | x22 | x51"
122 and 32: "x24 | x58 | x23 | x52"
123 and 33: "x59 | x24 | x53"
124 and 34: "x25 | x54"
125 and 35: "x26 | x25 | x55"
126 and 36: "x27 | x26 | x56"
127 and 37: "x28 | x27 | x57"
128 and 38: "x29 | x28 | x58"
129 and 39: "~x1 | ~x31"
130 and 40: "~x1 | ~x0"
131 and 41: "~x31 | ~x0"
132 and 42: "~x2 | ~x32"
133 and 43: "~x2 | ~x1"
134 and 44: "~x32 | ~x1"
135 and 45: "~x3 | ~x33"
136 and 46: "~x3 | ~x2"
137 and 47: "~x33 | ~x2"
138 and 48: "~x4 | ~x34"
139 and 49: "~x4 | ~x3"
140 and 50: "~x34 | ~x3"
141 and 51: "~x35 | ~x4"
142 and 52: "~x5 | ~x36"
143 and 53: "~x5 | ~x30"
144 and 54: "~x36 | ~x30"
145 and 55: "~x6 | ~x37"
146 and 56: "~x6 | ~x5"
147 and 57: "~x6 | ~x31"
148 and 58: "~x37 | ~x5"
149 and 59: "~x37 | ~x31"
150 and 60: "~x5 | ~x31"
151 and 61: "~x7 | ~x38"
152 and 62: "~x7 | ~x6"
153 and 63: "~x7 | ~x32"
154 and 64: "~x38 | ~x6"
155 and 65: "~x38 | ~x32"
156 and 66: "~x6 | ~x32"
157 and 67: "~x8 | ~x39"
158 and 68: "~x8 | ~x7"
159 and 69: "~x8 | ~x33"
160 and 70: "~x39 | ~x7"
161 and 71: "~x39 | ~x33"
162 and 72: "~x7 | ~x33"
163 and 73: "~x9 | ~x40"
164 and 74: "~x9 | ~x8"
165 and 75: "~x9 | ~x34"
166 and 76: "~x40 | ~x8"
167 and 77: "~x40 | ~x34"
168 and 78: "~x8 | ~x34"
169 and 79: "~x41 | ~x9"
170 and 80: "~x41 | ~x35"
171 and 81: "~x9 | ~x35"
172 and 82: "~x10 | ~x42"
173 and 83: "~x10 | ~x36"
174 and 84: "~x42 | ~x36"
175 and 85: "~x11 | ~x43"
176 and 86: "~x11 | ~x10"
177 and 87: "~x11 | ~x37"
178 and 88: "~x43 | ~x10"
179 and 89: "~x43 | ~x37"
180 and 90: "~x10 | ~x37"
181 and 91: "~x12 | ~x44"
182 and 92: "~x12 | ~x11"
183 and 93: "~x12 | ~x38"
184 and 94: "~x44 | ~x11"
185 and 95: "~x44 | ~x38"
186 and 96: "~x11 | ~x38"
187 and 97: "~x13 | ~x45"
188 and 98: "~x13 | ~x12"
189 and 99: "~x13 | ~x39"
190 and 100: "~x45 | ~x12"
191 and 101: "~x45 | ~x39"
192 and 102: "~x12 | ~x39"
193 and 103: "~x14 | ~x46"
194 and 104: "~x14 | ~x13"
195 and 105: "~x14 | ~x40"
196 and 106: "~x46 | ~x13"
197 and 107: "~x46 | ~x40"
198 and 108: "~x13 | ~x40"
199 and 109: "~x47 | ~x14"
200 and 110: "~x47 | ~x41"
201 and 111: "~x14 | ~x41"
202 and 112: "~x15 | ~x48"
203 and 113: "~x15 | ~x42"
204 and 114: "~x48 | ~x42"
205 and 115: "~x16 | ~x49"
206 and 116: "~x16 | ~x15"
207 and 117: "~x16 | ~x43"
208 and 118: "~x49 | ~x15"
209 and 119: "~x49 | ~x43"
210 and 120: "~x15 | ~x43"
211 and 121: "~x17 | ~x50"
212 and 122: "~x17 | ~x16"
213 and 123: "~x17 | ~x44"
214 and 124: "~x50 | ~x16"
215 and 125: "~x50 | ~x44"
216 and 126: "~x16 | ~x44"
217 and 127: "~x18 | ~x51"
218 and 128: "~x18 | ~x17"
219 and 129: "~x18 | ~x45"
220 and 130: "~x51 | ~x17"
221 and 131: "~x51 | ~x45"
222 and 132: "~x17 | ~x45"
223 and 133: "~x19 | ~x52"
224 and 134: "~x19 | ~x18"
225 and 135: "~x19 | ~x46"
226 and 136: "~x52 | ~x18"
227 and 137: "~x52 | ~x46"
228 and 138: "~x18 | ~x46"
229 and 139: "~x53 | ~x19"
230 and 140: "~x53 | ~x47"
231 and 141: "~x19 | ~x47"
232 and 142: "~x20 | ~x54"
233 and 143: "~x20 | ~x48"
234 and 144: "~x54 | ~x48"
235 and 145: "~x21 | ~x55"
236 and 146: "~x21 | ~x20"
237 and 147: "~x21 | ~x49"
238 and 148: "~x55 | ~x20"
239 and 149: "~x55 | ~x49"
240 and 150: "~x20 | ~x49"
241 and 151: "~x22 | ~x56"
242 and 152: "~x22 | ~x21"
243 and 153: "~x22 | ~x50"
244 and 154: "~x56 | ~x21"
245 and 155: "~x56 | ~x50"
246 and 156: "~x21 | ~x50"
247 and 157: "~x23 | ~x57"
248 and 158: "~x23 | ~x22"
249 and 159: "~x23 | ~x51"
250 and 160: "~x57 | ~x22"
251 and 161: "~x57 | ~x51"
252 and 162: "~x22 | ~x51"
253 and 163: "~x24 | ~x58"
254 and 164: "~x24 | ~x23"
255 and 165: "~x24 | ~x52"
256 and 166: "~x58 | ~x23"
257 and 167: "~x58 | ~x52"
258 and 168: "~x23 | ~x52"
259 and 169: "~x59 | ~x24"
260 and 170: "~x59 | ~x53"
261 and 171: "~x24 | ~x53"
262 and 172: "~x25 | ~x54"
263 and 173: "~x26 | ~x25"
264 and 174: "~x26 | ~x55"
265 and 175: "~x25 | ~x55"
266 and 176: "~x27 | ~x26"
267 and 177: "~x27 | ~x56"
268 and 178: "~x26 | ~x56"
269 and 179: "~x28 | ~x27"
270 and 180: "~x28 | ~x57"
271 and 181: "~x27 | ~x57"
272 and 182: "~x29 | ~x28"
273 and 183: "~x29 | ~x58"
274 and 184: "~x28 | ~x58"
275 shows "False"
276 using assms
277 (*
278 by sat
279 *)
280 by rawsat  -- {* this is without CNF conversion *}
282 (* Translated from TPTP problem library: MSC007-1.008.dimacs *)
284 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
285 and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
286 and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
287 and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
288 and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
289 and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
290 and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
291 and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
292 and 9: "~x0 | ~x7"
293 and 10: "~x0 | ~x14"
294 and 11: "~x0 | ~x21"
295 and 12: "~x0 | ~x28"
296 and 13: "~x0 | ~x35"
297 and 14: "~x0 | ~x42"
298 and 15: "~x0 | ~x49"
299 and 16: "~x7 | ~x14"
300 and 17: "~x7 | ~x21"
301 and 18: "~x7 | ~x28"
302 and 19: "~x7 | ~x35"
303 and 20: "~x7 | ~x42"
304 and 21: "~x7 | ~x49"
305 and 22: "~x14 | ~x21"
306 and 23: "~x14 | ~x28"
307 and 24: "~x14 | ~x35"
308 and 25: "~x14 | ~x42"
309 and 26: "~x14 | ~x49"
310 and 27: "~x21 | ~x28"
311 and 28: "~x21 | ~x35"
312 and 29: "~x21 | ~x42"
313 and 30: "~x21 | ~x49"
314 and 31: "~x28 | ~x35"
315 and 32: "~x28 | ~x42"
316 and 33: "~x28 | ~x49"
317 and 34: "~x35 | ~x42"
318 and 35: "~x35 | ~x49"
319 and 36: "~x42 | ~x49"
320 and 37: "~x1 | ~x8"
321 and 38: "~x1 | ~x15"
322 and 39: "~x1 | ~x22"
323 and 40: "~x1 | ~x29"
324 and 41: "~x1 | ~x36"
325 and 42: "~x1 | ~x43"
326 and 43: "~x1 | ~x50"
327 and 44: "~x8 | ~x15"
328 and 45: "~x8 | ~x22"
329 and 46: "~x8 | ~x29"
330 and 47: "~x8 | ~x36"
331 and 48: "~x8 | ~x43"
332 and 49: "~x8 | ~x50"
333 and 50: "~x15 | ~x22"
334 and 51: "~x15 | ~x29"
335 and 52: "~x15 | ~x36"
336 and 53: "~x15 | ~x43"
337 and 54: "~x15 | ~x50"
338 and 55: "~x22 | ~x29"
339 and 56: "~x22 | ~x36"
340 and 57: "~x22 | ~x43"
341 and 58: "~x22 | ~x50"
342 and 59: "~x29 | ~x36"
343 and 60: "~x29 | ~x43"
344 and 61: "~x29 | ~x50"
345 and 62: "~x36 | ~x43"
346 and 63: "~x36 | ~x50"
347 and 64: "~x43 | ~x50"
348 and 65: "~x2 | ~x9"
349 and 66: "~x2 | ~x16"
350 and 67: "~x2 | ~x23"
351 and 68: "~x2 | ~x30"
352 and 69: "~x2 | ~x37"
353 and 70: "~x2 | ~x44"
354 and 71: "~x2 | ~x51"
355 and 72: "~x9 | ~x16"
356 and 73: "~x9 | ~x23"
357 and 74: "~x9 | ~x30"
358 and 75: "~x9 | ~x37"
359 and 76: "~x9 | ~x44"
360 and 77: "~x9 | ~x51"
361 and 78: "~x16 | ~x23"
362 and 79: "~x16 | ~x30"
363 and 80: "~x16 | ~x37"
364 and 81: "~x16 | ~x44"
365 and 82: "~x16 | ~x51"
366 and 83: "~x23 | ~x30"
367 and 84: "~x23 | ~x37"
368 and 85: "~x23 | ~x44"
369 and 86: "~x23 | ~x51"
370 and 87: "~x30 | ~x37"
371 and 88: "~x30 | ~x44"
372 and 89: "~x30 | ~x51"
373 and 90: "~x37 | ~x44"
374 and 91: "~x37 | ~x51"
375 and 92: "~x44 | ~x51"
376 and 93: "~x3 | ~x10"
377 and 94: "~x3 | ~x17"
378 and 95: "~x3 | ~x24"
379 and 96: "~x3 | ~x31"
380 and 97: "~x3 | ~x38"
381 and 98: "~x3 | ~x45"
382 and 99: "~x3 | ~x52"
383 and 100: "~x10 | ~x17"
384 and 101: "~x10 | ~x24"
385 and 102: "~x10 | ~x31"
386 and 103: "~x10 | ~x38"
387 and 104: "~x10 | ~x45"
388 and 105: "~x10 | ~x52"
389 and 106: "~x17 | ~x24"
390 and 107: "~x17 | ~x31"
391 and 108: "~x17 | ~x38"
392 and 109: "~x17 | ~x45"
393 and 110: "~x17 | ~x52"
394 and 111: "~x24 | ~x31"
395 and 112: "~x24 | ~x38"
396 and 113: "~x24 | ~x45"
397 and 114: "~x24 | ~x52"
398 and 115: "~x31 | ~x38"
399 and 116: "~x31 | ~x45"
400 and 117: "~x31 | ~x52"
401 and 118: "~x38 | ~x45"
402 and 119: "~x38 | ~x52"
403 and 120: "~x45 | ~x52"
404 and 121: "~x4 | ~x11"
405 and 122: "~x4 | ~x18"
406 and 123: "~x4 | ~x25"
407 and 124: "~x4 | ~x32"
408 and 125: "~x4 | ~x39"
409 and 126: "~x4 | ~x46"
410 and 127: "~x4 | ~x53"
411 and 128: "~x11 | ~x18"
412 and 129: "~x11 | ~x25"
413 and 130: "~x11 | ~x32"
414 and 131: "~x11 | ~x39"
415 and 132: "~x11 | ~x46"
416 and 133: "~x11 | ~x53"
417 and 134: "~x18 | ~x25"
418 and 135: "~x18 | ~x32"
419 and 136: "~x18 | ~x39"
420 and 137: "~x18 | ~x46"
421 and 138: "~x18 | ~x53"
422 and 139: "~x25 | ~x32"
423 and 140: "~x25 | ~x39"
424 and 141: "~x25 | ~x46"
425 and 142: "~x25 | ~x53"
426 and 143: "~x32 | ~x39"
427 and 144: "~x32 | ~x46"
428 and 145: "~x32 | ~x53"
429 and 146: "~x39 | ~x46"
430 and 147: "~x39 | ~x53"
431 and 148: "~x46 | ~x53"
432 and 149: "~x5 | ~x12"
433 and 150: "~x5 | ~x19"
434 and 151: "~x5 | ~x26"
435 and 152: "~x5 | ~x33"
436 and 153: "~x5 | ~x40"
437 and 154: "~x5 | ~x47"
438 and 155: "~x5 | ~x54"
439 and 156: "~x12 | ~x19"
440 and 157: "~x12 | ~x26"
441 and 158: "~x12 | ~x33"
442 and 159: "~x12 | ~x40"
443 and 160: "~x12 | ~x47"
444 and 161: "~x12 | ~x54"
445 and 162: "~x19 | ~x26"
446 and 163: "~x19 | ~x33"
447 and 164: "~x19 | ~x40"
448 and 165: "~x19 | ~x47"
449 and 166: "~x19 | ~x54"
450 and 167: "~x26 | ~x33"
451 and 168: "~x26 | ~x40"
452 and 169: "~x26 | ~x47"
453 and 170: "~x26 | ~x54"
454 and 171: "~x33 | ~x40"
455 and 172: "~x33 | ~x47"
456 and 173: "~x33 | ~x54"
457 and 174: "~x40 | ~x47"
458 and 175: "~x40 | ~x54"
459 and 176: "~x47 | ~x54"
460 and 177: "~x6 | ~x13"
461 and 178: "~x6 | ~x20"
462 and 179: "~x6 | ~x27"
463 and 180: "~x6 | ~x34"
464 and 181: "~x6 | ~x41"
465 and 182: "~x6 | ~x48"
466 and 183: "~x6 | ~x55"
467 and 184: "~x13 | ~x20"
468 and 185: "~x13 | ~x27"
469 and 186: "~x13 | ~x34"
470 and 187: "~x13 | ~x41"
471 and 188: "~x13 | ~x48"
472 and 189: "~x13 | ~x55"
473 and 190: "~x20 | ~x27"
474 and 191: "~x20 | ~x34"
475 and 192: "~x20 | ~x41"
476 and 193: "~x20 | ~x48"
477 and 194: "~x20 | ~x55"
478 and 195: "~x27 | ~x34"
479 and 196: "~x27 | ~x41"
480 and 197: "~x27 | ~x48"
481 and 198: "~x27 | ~x55"
482 and 199: "~x34 | ~x41"
483 and 200: "~x34 | ~x48"
484 and 201: "~x34 | ~x55"
485 and 202: "~x41 | ~x48"
486 and 203: "~x41 | ~x55"
487 and 204: "~x48 | ~x55"
488 shows "False"
489 using assms
490 (*
491 by sat
492 *)
493 by rawsat  -- {* this is without CNF conversion *}
495 (* Old sequent clause representation ("[c_i, p, ~q, \<dots>] \<turnstile> False"):
496    sat, zchaff_with_proofs: 8705 resolution steps in
497                             +++ User 1.154  All 1.189 secs
498    sat, minisat_with_proofs: 40790 resolution steps in
499                              +++ User 3.762  All 3.806 secs
501    rawsat, zchaff_with_proofs: 8705 resolution steps in
502                                +++ User 0.731  All 0.751 secs
503    rawsat, minisat_with_proofs: 40790 resolution steps in
504                                 +++ User 3.514  All 3.550 secs
506    CNF clause representation ("[c_1 && \<dots> && c_n, p, ~q, \<dots>] \<turnstile> False"):
507    rawsat, zchaff_with_proofs: 8705 resolution steps in
508                                +++ User 0.653  All 0.670 secs
509    rawsat, minisat_with_proofs: 40790 resolution steps in
510                                 +++ User 1.860  All 1.886 secs
512    (as of 2006-08-30, on a 2.5 GHz Pentium 4)
513 *)
515 (* ML {* Toplevel.profiling := 0; *} *)
517 text {*
518 Function {\tt benchmark} takes the name of an existing DIMACS CNF
519 file, parses this file, passes the problem to a SAT solver, and checks
520 the proof of unsatisfiability found by the solver.  The function
521 measures the time spent on proof reconstruction (at least real time
522 also includes time spent in the SAT solver), and additionally returns
523 the number of resolution steps in the proof.
524 *}
526 (* ML {*
527 sat.solver := "zchaff_with_proofs";
528 sat.trace_sat := false;
529 quick_and_dirty := false;
530 *} *)
532 ML {*
533 fun benchmark dimacsfile =
534 let
535   val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
536   fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
537     | and_to_list fm acc = rev (fm :: acc)
538   val clauses = and_to_list prop_fm []
539   val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
540   val cterms = map (Thm.cterm_of @{theory}) terms
541   val start = Timing.start ()
542   val thm = sat.rawsat_thm @{context} cterms
543 in
544   (Timing.result start, ! sat.counter)
545 end;
546 *}
548 end