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