src/HOL/ex/SAT_Examples.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 19236 150e8b0fb991
child 19534 1724ec4032c5
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/ex/SAT_Examples.thy
     2     ID:         $Id$
     3     Author:     Alwen Tiu, Tjark Weber
     4     Copyright   2005-2006
     5 *)
     6 
     7 header {* Examples for the 'sat' and 'satx' tactic *}
     8 
     9 theory SAT_Examples imports Main
    10 
    11 begin
    12 
    13 ML {* set sat.trace_sat; *}
    14 ML {* set quick_and_dirty; *}
    15 
    16 lemma "True"
    17 by sat
    18 
    19 lemma "a | ~a"
    20 by sat
    21 
    22 lemma "(a | b) & ~a \<Longrightarrow> b"
    23 by sat
    24 
    25 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    26 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    27 by sat
    28 
    29 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
    30 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    31 apply (erule exE | erule conjE)+
    32 by satx
    33 
    34 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
    35   (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    36 apply (tactic {* cnf.cnf_rewrite_tac 1 *})
    37 by sat
    38 
    39 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
    40   (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
    41 apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
    42 apply (erule exE | erule conjE)+
    43 by satx
    44 
    45 lemma "P=P=P=P=P=P=P=P=P=P"
    46 by sat
    47 
    48 lemma "P=P=P=P=P=P=P=P=P=P"
    49 by satx
    50 
    51 lemma  "!! a b c. [| a | b | c | d ;
    52 e | f | (a & d) ;
    53 ~(a | (c & ~c)) | b ;
    54 ~(b & (x | ~x)) | c ;
    55 ~(d | False) | c ;
    56 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
    57 by sat
    58 
    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 satx
    66 
    67 ML {* reset sat.trace_sat; *}
    68 ML {* reset quick_and_dirty; *}
    69 
    70 ML {* Toplevel.profiling := 1; *}
    71 
    72 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
    73 
    74 lemma assumes 1: "~x0"
    75 and 2: "~x30"
    76 and 3: "~x29"
    77 and 4: "~x59"
    78 and 5: "x1 | x31 | x0"
    79 and 6: "x2 | x32 | x1"
    80 and 7: "x3 | x33 | x2"
    81 and 8: "x4 | x34 | x3"
    82 and 9: "x35 | x4"
    83 and 10: "x5 | x36 | x30"
    84 and 11: "x6 | x37 | x5 | x31"
    85 and 12: "x7 | x38 | x6 | x32"
    86 and 13: "x8 | x39 | x7 | x33"
    87 and 14: "x9 | x40 | x8 | x34"
    88 and 15: "x41 | x9 | x35"
    89 and 16: "x10 | x42 | x36"
    90 and 17: "x11 | x43 | x10 | x37"
    91 and 18: "x12 | x44 | x11 | x38"
    92 and 19: "x13 | x45 | x12 | x39"
    93 and 20: "x14 | x46 | x13 | x40"
    94 and 21: "x47 | x14 | x41"
    95 and 22: "x15 | x48 | x42"
    96 and 23: "x16 | x49 | x15 | x43"
    97 and 24: "x17 | x50 | x16 | x44"
    98 and 25: "x18 | x51 | x17 | x45"
    99 and 26: "x19 | x52 | x18 | x46"
   100 and 27: "x53 | x19 | x47"
   101 and 28: "x20 | x54 | x48"
   102 and 29: "x21 | x55 | x20 | x49"
   103 and 30: "x22 | x56 | x21 | x50"
   104 and 31: "x23 | x57 | x22 | x51"
   105 and 32: "x24 | x58 | x23 | x52"
   106 and 33: "x59 | x24 | x53"
   107 and 34: "x25 | x54"
   108 and 35: "x26 | x25 | x55"
   109 and 36: "x27 | x26 | x56"
   110 and 37: "x28 | x27 | x57"
   111 and 38: "x29 | x28 | x58"
   112 and 39: "~x1 | ~x31"
   113 and 40: "~x1 | ~x0"
   114 and 41: "~x31 | ~x0"
   115 and 42: "~x2 | ~x32"
   116 and 43: "~x2 | ~x1"
   117 and 44: "~x32 | ~x1"
   118 and 45: "~x3 | ~x33"
   119 and 46: "~x3 | ~x2"
   120 and 47: "~x33 | ~x2"
   121 and 48: "~x4 | ~x34"
   122 and 49: "~x4 | ~x3"
   123 and 50: "~x34 | ~x3"
   124 and 51: "~x35 | ~x4"
   125 and 52: "~x5 | ~x36"
   126 and 53: "~x5 | ~x30"
   127 and 54: "~x36 | ~x30"
   128 and 55: "~x6 | ~x37"
   129 and 56: "~x6 | ~x5"
   130 and 57: "~x6 | ~x31"
   131 and 58: "~x37 | ~x5"
   132 and 59: "~x37 | ~x31"
   133 and 60: "~x5 | ~x31"
   134 and 61: "~x7 | ~x38"
   135 and 62: "~x7 | ~x6"
   136 and 63: "~x7 | ~x32"
   137 and 64: "~x38 | ~x6"
   138 and 65: "~x38 | ~x32"
   139 and 66: "~x6 | ~x32"
   140 and 67: "~x8 | ~x39"
   141 and 68: "~x8 | ~x7"
   142 and 69: "~x8 | ~x33"
   143 and 70: "~x39 | ~x7"
   144 and 71: "~x39 | ~x33"
   145 and 72: "~x7 | ~x33"
   146 and 73: "~x9 | ~x40"
   147 and 74: "~x9 | ~x8"
   148 and 75: "~x9 | ~x34"
   149 and 76: "~x40 | ~x8"
   150 and 77: "~x40 | ~x34"
   151 and 78: "~x8 | ~x34"
   152 and 79: "~x41 | ~x9"
   153 and 80: "~x41 | ~x35"
   154 and 81: "~x9 | ~x35"
   155 and 82: "~x10 | ~x42"
   156 and 83: "~x10 | ~x36"
   157 and 84: "~x42 | ~x36"
   158 and 85: "~x11 | ~x43"
   159 and 86: "~x11 | ~x10"
   160 and 87: "~x11 | ~x37"
   161 and 88: "~x43 | ~x10"
   162 and 89: "~x43 | ~x37"
   163 and 90: "~x10 | ~x37"
   164 and 91: "~x12 | ~x44"
   165 and 92: "~x12 | ~x11"
   166 and 93: "~x12 | ~x38"
   167 and 94: "~x44 | ~x11"
   168 and 95: "~x44 | ~x38"
   169 and 96: "~x11 | ~x38"
   170 and 97: "~x13 | ~x45"
   171 and 98: "~x13 | ~x12"
   172 and 99: "~x13 | ~x39"
   173 and 100: "~x45 | ~x12"
   174 and 101: "~x45 | ~x39"
   175 and 102: "~x12 | ~x39"
   176 and 103: "~x14 | ~x46"
   177 and 104: "~x14 | ~x13"
   178 and 105: "~x14 | ~x40"
   179 and 106: "~x46 | ~x13"
   180 and 107: "~x46 | ~x40"
   181 and 108: "~x13 | ~x40"
   182 and 109: "~x47 | ~x14"
   183 and 110: "~x47 | ~x41"
   184 and 111: "~x14 | ~x41"
   185 and 112: "~x15 | ~x48"
   186 and 113: "~x15 | ~x42"
   187 and 114: "~x48 | ~x42"
   188 and 115: "~x16 | ~x49"
   189 and 116: "~x16 | ~x15"
   190 and 117: "~x16 | ~x43"
   191 and 118: "~x49 | ~x15"
   192 and 119: "~x49 | ~x43"
   193 and 120: "~x15 | ~x43"
   194 and 121: "~x17 | ~x50"
   195 and 122: "~x17 | ~x16"
   196 and 123: "~x17 | ~x44"
   197 and 124: "~x50 | ~x16"
   198 and 125: "~x50 | ~x44"
   199 and 126: "~x16 | ~x44"
   200 and 127: "~x18 | ~x51"
   201 and 128: "~x18 | ~x17"
   202 and 129: "~x18 | ~x45"
   203 and 130: "~x51 | ~x17"
   204 and 131: "~x51 | ~x45"
   205 and 132: "~x17 | ~x45"
   206 and 133: "~x19 | ~x52"
   207 and 134: "~x19 | ~x18"
   208 and 135: "~x19 | ~x46"
   209 and 136: "~x52 | ~x18"
   210 and 137: "~x52 | ~x46"
   211 and 138: "~x18 | ~x46"
   212 and 139: "~x53 | ~x19"
   213 and 140: "~x53 | ~x47"
   214 and 141: "~x19 | ~x47"
   215 and 142: "~x20 | ~x54"
   216 and 143: "~x20 | ~x48"
   217 and 144: "~x54 | ~x48"
   218 and 145: "~x21 | ~x55"
   219 and 146: "~x21 | ~x20"
   220 and 147: "~x21 | ~x49"
   221 and 148: "~x55 | ~x20"
   222 and 149: "~x55 | ~x49"
   223 and 150: "~x20 | ~x49"
   224 and 151: "~x22 | ~x56"
   225 and 152: "~x22 | ~x21"
   226 and 153: "~x22 | ~x50"
   227 and 154: "~x56 | ~x21"
   228 and 155: "~x56 | ~x50"
   229 and 156: "~x21 | ~x50"
   230 and 157: "~x23 | ~x57"
   231 and 158: "~x23 | ~x22"
   232 and 159: "~x23 | ~x51"
   233 and 160: "~x57 | ~x22"
   234 and 161: "~x57 | ~x51"
   235 and 162: "~x22 | ~x51"
   236 and 163: "~x24 | ~x58"
   237 and 164: "~x24 | ~x23"
   238 and 165: "~x24 | ~x52"
   239 and 166: "~x58 | ~x23"
   240 and 167: "~x58 | ~x52"
   241 and 168: "~x23 | ~x52"
   242 and 169: "~x59 | ~x24"
   243 and 170: "~x59 | ~x53"
   244 and 171: "~x24 | ~x53"
   245 and 172: "~x25 | ~x54"
   246 and 173: "~x26 | ~x25"
   247 and 174: "~x26 | ~x55"
   248 and 175: "~x25 | ~x55"
   249 and 176: "~x27 | ~x26"
   250 and 177: "~x27 | ~x56"
   251 and 178: "~x26 | ~x56"
   252 and 179: "~x28 | ~x27"
   253 and 180: "~x28 | ~x57"
   254 and 181: "~x27 | ~x57"
   255 and 182: "~x29 | ~x28"
   256 and 183: "~x29 | ~x58"
   257 and 184: "~x28 | ~x58"
   258 shows "False"
   259 using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
   260 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
   261 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
   262 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
   263 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
   264 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
   265 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
   266 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
   267 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
   268 180 181 182 183 184
   269 by sat
   270 
   271 (* Translated from TPTP problem library: MSC007-1.008.dimacs *)
   272 
   273 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
   274 and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
   275 and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
   276 and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
   277 and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
   278 and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
   279 and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
   280 and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
   281 and 9: "~x0 | ~x7"
   282 and 10: "~x0 | ~x14"
   283 and 11: "~x0 | ~x21"
   284 and 12: "~x0 | ~x28"
   285 and 13: "~x0 | ~x35"
   286 and 14: "~x0 | ~x42"
   287 and 15: "~x0 | ~x49"
   288 and 16: "~x7 | ~x14"
   289 and 17: "~x7 | ~x21"
   290 and 18: "~x7 | ~x28"
   291 and 19: "~x7 | ~x35"
   292 and 20: "~x7 | ~x42"
   293 and 21: "~x7 | ~x49"
   294 and 22: "~x14 | ~x21"
   295 and 23: "~x14 | ~x28"
   296 and 24: "~x14 | ~x35"
   297 and 25: "~x14 | ~x42"
   298 and 26: "~x14 | ~x49"
   299 and 27: "~x21 | ~x28"
   300 and 28: "~x21 | ~x35"
   301 and 29: "~x21 | ~x42"
   302 and 30: "~x21 | ~x49"
   303 and 31: "~x28 | ~x35"
   304 and 32: "~x28 | ~x42"
   305 and 33: "~x28 | ~x49"
   306 and 34: "~x35 | ~x42"
   307 and 35: "~x35 | ~x49"
   308 and 36: "~x42 | ~x49"
   309 and 37: "~x1 | ~x8"
   310 and 38: "~x1 | ~x15"
   311 and 39: "~x1 | ~x22"
   312 and 40: "~x1 | ~x29"
   313 and 41: "~x1 | ~x36"
   314 and 42: "~x1 | ~x43"
   315 and 43: "~x1 | ~x50"
   316 and 44: "~x8 | ~x15"
   317 and 45: "~x8 | ~x22"
   318 and 46: "~x8 | ~x29"
   319 and 47: "~x8 | ~x36"
   320 and 48: "~x8 | ~x43"
   321 and 49: "~x8 | ~x50"
   322 and 50: "~x15 | ~x22"
   323 and 51: "~x15 | ~x29"
   324 and 52: "~x15 | ~x36"
   325 and 53: "~x15 | ~x43"
   326 and 54: "~x15 | ~x50"
   327 and 55: "~x22 | ~x29"
   328 and 56: "~x22 | ~x36"
   329 and 57: "~x22 | ~x43"
   330 and 58: "~x22 | ~x50"
   331 and 59: "~x29 | ~x36"
   332 and 60: "~x29 | ~x43"
   333 and 61: "~x29 | ~x50"
   334 and 62: "~x36 | ~x43"
   335 and 63: "~x36 | ~x50"
   336 and 64: "~x43 | ~x50"
   337 and 65: "~x2 | ~x9"
   338 and 66: "~x2 | ~x16"
   339 and 67: "~x2 | ~x23"
   340 and 68: "~x2 | ~x30"
   341 and 69: "~x2 | ~x37"
   342 and 70: "~x2 | ~x44"
   343 and 71: "~x2 | ~x51"
   344 and 72: "~x9 | ~x16"
   345 and 73: "~x9 | ~x23"
   346 and 74: "~x9 | ~x30"
   347 and 75: "~x9 | ~x37"
   348 and 76: "~x9 | ~x44"
   349 and 77: "~x9 | ~x51"
   350 and 78: "~x16 | ~x23"
   351 and 79: "~x16 | ~x30"
   352 and 80: "~x16 | ~x37"
   353 and 81: "~x16 | ~x44"
   354 and 82: "~x16 | ~x51"
   355 and 83: "~x23 | ~x30"
   356 and 84: "~x23 | ~x37"
   357 and 85: "~x23 | ~x44"
   358 and 86: "~x23 | ~x51"
   359 and 87: "~x30 | ~x37"
   360 and 88: "~x30 | ~x44"
   361 and 89: "~x30 | ~x51"
   362 and 90: "~x37 | ~x44"
   363 and 91: "~x37 | ~x51"
   364 and 92: "~x44 | ~x51"
   365 and 93: "~x3 | ~x10"
   366 and 94: "~x3 | ~x17"
   367 and 95: "~x3 | ~x24"
   368 and 96: "~x3 | ~x31"
   369 and 97: "~x3 | ~x38"
   370 and 98: "~x3 | ~x45"
   371 and 99: "~x3 | ~x52"
   372 and 100: "~x10 | ~x17"
   373 and 101: "~x10 | ~x24"
   374 and 102: "~x10 | ~x31"
   375 and 103: "~x10 | ~x38"
   376 and 104: "~x10 | ~x45"
   377 and 105: "~x10 | ~x52"
   378 and 106: "~x17 | ~x24"
   379 and 107: "~x17 | ~x31"
   380 and 108: "~x17 | ~x38"
   381 and 109: "~x17 | ~x45"
   382 and 110: "~x17 | ~x52"
   383 and 111: "~x24 | ~x31"
   384 and 112: "~x24 | ~x38"
   385 and 113: "~x24 | ~x45"
   386 and 114: "~x24 | ~x52"
   387 and 115: "~x31 | ~x38"
   388 and 116: "~x31 | ~x45"
   389 and 117: "~x31 | ~x52"
   390 and 118: "~x38 | ~x45"
   391 and 119: "~x38 | ~x52"
   392 and 120: "~x45 | ~x52"
   393 and 121: "~x4 | ~x11"
   394 and 122: "~x4 | ~x18"
   395 and 123: "~x4 | ~x25"
   396 and 124: "~x4 | ~x32"
   397 and 125: "~x4 | ~x39"
   398 and 126: "~x4 | ~x46"
   399 and 127: "~x4 | ~x53"
   400 and 128: "~x11 | ~x18"
   401 and 129: "~x11 | ~x25"
   402 and 130: "~x11 | ~x32"
   403 and 131: "~x11 | ~x39"
   404 and 132: "~x11 | ~x46"
   405 and 133: "~x11 | ~x53"
   406 and 134: "~x18 | ~x25"
   407 and 135: "~x18 | ~x32"
   408 and 136: "~x18 | ~x39"
   409 and 137: "~x18 | ~x46"
   410 and 138: "~x18 | ~x53"
   411 and 139: "~x25 | ~x32"
   412 and 140: "~x25 | ~x39"
   413 and 141: "~x25 | ~x46"
   414 and 142: "~x25 | ~x53"
   415 and 143: "~x32 | ~x39"
   416 and 144: "~x32 | ~x46"
   417 and 145: "~x32 | ~x53"
   418 and 146: "~x39 | ~x46"
   419 and 147: "~x39 | ~x53"
   420 and 148: "~x46 | ~x53"
   421 and 149: "~x5 | ~x12"
   422 and 150: "~x5 | ~x19"
   423 and 151: "~x5 | ~x26"
   424 and 152: "~x5 | ~x33"
   425 and 153: "~x5 | ~x40"
   426 and 154: "~x5 | ~x47"
   427 and 155: "~x5 | ~x54"
   428 and 156: "~x12 | ~x19"
   429 and 157: "~x12 | ~x26"
   430 and 158: "~x12 | ~x33"
   431 and 159: "~x12 | ~x40"
   432 and 160: "~x12 | ~x47"
   433 and 161: "~x12 | ~x54"
   434 and 162: "~x19 | ~x26"
   435 and 163: "~x19 | ~x33"
   436 and 164: "~x19 | ~x40"
   437 and 165: "~x19 | ~x47"
   438 and 166: "~x19 | ~x54"
   439 and 167: "~x26 | ~x33"
   440 and 168: "~x26 | ~x40"
   441 and 169: "~x26 | ~x47"
   442 and 170: "~x26 | ~x54"
   443 and 171: "~x33 | ~x40"
   444 and 172: "~x33 | ~x47"
   445 and 173: "~x33 | ~x54"
   446 and 174: "~x40 | ~x47"
   447 and 175: "~x40 | ~x54"
   448 and 176: "~x47 | ~x54"
   449 and 177: "~x6 | ~x13"
   450 and 178: "~x6 | ~x20"
   451 and 179: "~x6 | ~x27"
   452 and 180: "~x6 | ~x34"
   453 and 181: "~x6 | ~x41"
   454 and 182: "~x6 | ~x48"
   455 and 183: "~x6 | ~x55"
   456 and 184: "~x13 | ~x20"
   457 and 185: "~x13 | ~x27"
   458 and 186: "~x13 | ~x34"
   459 and 187: "~x13 | ~x41"
   460 and 188: "~x13 | ~x48"
   461 and 189: "~x13 | ~x55"
   462 and 190: "~x20 | ~x27"
   463 and 191: "~x20 | ~x34"
   464 and 192: "~x20 | ~x41"
   465 and 193: "~x20 | ~x48"
   466 and 194: "~x20 | ~x55"
   467 and 195: "~x27 | ~x34"
   468 and 196: "~x27 | ~x41"
   469 and 197: "~x27 | ~x48"
   470 and 198: "~x27 | ~x55"
   471 and 199: "~x34 | ~x41"
   472 and 200: "~x34 | ~x48"
   473 and 201: "~x34 | ~x55"
   474 and 202: "~x41 | ~x48"
   475 and 203: "~x41 | ~x55"
   476 and 204: "~x48 | ~x55"
   477 shows "False"
   478 using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
   479 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
   480 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
   481 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
   482 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
   483 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
   484 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
   485 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
   486 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
   487 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
   488 200 201 202 203 204
   489 by sat
   490 
   491 ML {* Toplevel.profiling := 0; *}
   492 
   493 end