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