OKlibrary  0.2.1.6
uhit_def.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 30.4.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009, 2011, 2012, 2013 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Deficiency2.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/tests/SetSystems.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00032 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/DP-Reductions.mac")$
00033 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Deficiency3.mac")$
00034 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac")$
00035 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00037 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00038 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")$
00039 
00040 
00041 /* kill(uhit_def)$ */
00042 
00043 /* The list of available deficiencies. */
00044 uhit_def[0,"info"] : append(create_list(k,k,1,28),[43,58,59])$
00045 
00046 /* For a given deficiency k, the info-field uhit_def[k,"info"] contains:
00047  - true if the classification is complete, and false/unknown otherwise
00048  - the smallest possible n resp. a lower bound
00049  - the largest possible n resp. an upper bound
00050  - the list of available n-values, represented as pairs [n,true/false/unknown],
00051    stating whether or not for this n the list is complete.
00052 */
00053 /* Complete means that every possible isomorphism type is
00054    represented (exactly once). */
00055 /* "false" here means that definitely some cases are missing. */
00056 
00057 
00058 /* Deficiency 1 */
00059 
00060 uhit_def[1,"info"] : [true,0,0,[[0,true]]]$
00061 uhit_def[1,0] : [{{}}]$
00062 
00063 
00064 /* Deficiency 2 */
00065 
00066 uhit_def[2,"info"] : [true,2,3,[[2,true],[3,true]]]$
00067 uhit_def[2,2] : [musatd2_fcs(2)[2]]$
00068 uhit_def[2,3] : [max_var_hitting_def(2)[2]]$
00069 
00070 
00071 /* Deficiency 3 */
00072 
00073 uhit_def[3,"info"] : [unknown,3,inf,[[3,true],[4,true],[5,unknown],[6,unknown],[7,unknown]]]$
00074 uhit_def[3,3] : [
00075  minvdegdef3(2)[2],
00076  {{1,2,3},{-1,2,3},{1,-2,3},{-1,-2,3},{1,-3},{-1,-3}},
00077  {{-3,-2},{-3,-1,2},{-3,1,2},{-2,-1,3},{-2,1,3},{2,3}}
00078 ]$
00079 uhit_def[3,4] : [
00080  {{-4,-3},{-4,-1,2,3},{-4,1,2,3},{-3,-2,4},{-2,-1,3},{-2,1,3},{2,4}},
00081  {{-4,-3},{-4,-1,2,3},{-4,1,2,3},{-3,4},{-2,-1,3},{-2,1,3},{2,3,4}},
00082  {{-4,-3},{-4,-1,2,3},{-4,1,3},{-3,-2,-1,4},{-2,-1,3},{-2,1,4},{2,4}},
00083  {{-4,-3},{-4,2,3},{-3,-2,1,4},{-3,-1,4},{-2,3},{-1,2,3,4},{1,2,4}},
00084  {{-4,-3},{-4,2,3},{-3,-1,4},{-3,1,4},{-2,-1,3},{-2,1,3},{2,3,4}},
00085  {{-4,-3,-2},{-4,-2,3},{-3,-2,-1,4},{-3,-2,1,4},{-2,3,4},{-1,2},{1,2}},
00086  {{-4,-3,-2},{-4,2},{-3,-1,4},{-3,1,4},{-2,-1,3},{-2,1,3},{2,3,4}},
00087  {{-4,-3,-1},{-4,-3,1,2},{-4,-2,-1,3},{-4,-2,1},{-4,2,3},{-3,4},{3,4}},
00088  {{1,2,3,4},{-1,2},{-2,3},{-3,1},{-1,-2,-3,4},{-4,1,2,3},{-1,-2,-3,-4}},
00089  {{-4,-3},{-4,-2,-1,3},{-4,-2,1,3},{-4,-1,2,3},{-4,1,2,3},{-3,4},{3,4}}
00090 ]$
00091 uhit_def[3,5] : [
00092  vardisjoint_full_gluing(musatd2_fcs(2),musatd2_fcs(2))[2],
00093  {{1,2,3},{-1,2,3},{1,-2,4},{-1,-2,4},{2,-3,5},{2,-3,-5},{-2,-4,5},{-2,-4,-5}},
00094  {{-5,-4,-2},{-5,-2,3,4},{-4,-3,-2,5},{-3,-2,-1,4},{-3,-2,1,4},{-2,3,5},{-1,2},{1,2}},
00095  {{-5,-4,-2,-1},{-5,-4,-2,1},{-5,-2,-1,4},{-5,-2,1,4},{-5,2,3},{-3,-2,5},{-3,2},{3,5}},
00096  {{-5,-4},{-5,4},{-4,5},{-3,-2,-1,4,5},{-3,1,4,5},{-2,3,4,5},{-1,2,4,5},{1,2,3,4,5}},
00097  {{-5,-4},{-5,-3,4},{-4,-2,-1,3,5},{-4,-2,1,3,5},{-4,-1,2,3,5},{-4,1,2,3,5},{-3,5},{3,4}},
00098  {{-5,-4},{-5,4},{-4,-3,5},{-3,4,5},{-2,-1,3,5},{-2,1,3,5},{-1,2,3,5},{1,2,3,5}},
00099  {{-5,-4},{-5,4},{-4,-2,-1,3,5},{-3,-2,5},{-3,1,2,5},{-2,-1,3,4,5},{-1,2,5},{1,3,5}},
00100  {{-5,-4},{-5,4},{-4,-1,3,5},{-3,-2,5},{-3,2,5},{-2,1,3,5},{-1,3,4,5},{1,2,3,5}}
00101 ]$
00102 uhit_def[3,6] : [
00103  vardisjoint_full_gluing(musatd2_fcs(2),musatd2_fcs(3))[2],
00104  {{-6,-1},{-6,1},{-5,-4,-3,-2,6},{-5,-4,2,6},{-4,-3,5,6},{-4,-2,3,6},{-4,2,3,5,6},{-1,4,6},{1,4,6}},
00105  {{-6,-5,-4,1,2,3},{-6,1,2,3,4},{-5,1,2,3,6},{-4,1,2,3,5},{-3,-2,-1},{-3,1},{-2,3},{-1,2},{1,2,3,4,5,6}}, /* twisting_var_disjoint_cs(musatd2_fcs(3), {1,2,3}, musatd2_fcs(3)) */
00106  {{-6,-5,-4,-1,2},{-6,-1,2,4},{-5,-1,2,6},{-4,-1,2,5},{-3,-2,-1},{-3,1},{-2,3},{-1,2,4,5,6},{1,2,3}} /* twisting_var_disjoint_cs(musatd2_fcs(3), {-1,2}, musatd2_fcs(3)) */
00107 ]$
00108 uhit_def[3,7] : [
00109  max_var_hitting_def(3)[2]
00110 ]$
00111 
00112 
00113 
00114 /* Deficiency 4 */
00115 
00116 uhit_def[4,"info"] : [false,3,inf,[[3,true],[4,true],[5,unknown],[6,unknown],[7,unknown],[8,unknown],[9,unknown],[10,unknown],[11,unknown]]]$
00117 uhit_def[4,3] : [
00118  nearly_full_hitting_fcs(3)[2]
00119 ]$
00120 /* Remark: This is also minvdegdef4(2) (flipping variable 2). */
00121 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def4.mac")$
00122 uhit_def[4,11] : [
00123   max_var_hitting_def(4)[2]
00124 ]$
00125 
00126 
00127 /* Deficiency 5 */
00128 
00129 uhit_def[5,"info"] : [false,3,inf,[[3,true],[4,true],[5,false],[14,unknown],[15,unknown]]]$
00130 uhit_def[5,3] : [
00131  full_fcs(3)[2]
00132 ]$
00133 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def5.mac")$
00134 uhit_def[5,14] : [
00135  {{-14,-13,-12},{-14,-13,12},{-14,-12,13},{-14,12,13},{-11,-10,-9,-8,14},{-11,-10,8,14},
00136   {-11,-9,10,14},{-11,-8,9,14},{-11,8,9,10,14},{-7,-6,-5,-4,11,14},{-7,-6,4,11,14},
00137   {-7,-5,6,11,14},{-7,-4,5,11,14},{-7,4,5,6,11,14},{-3,-2,-1,7,11,14},{-3,1,7,11,14},
00138   {-2,3,7,11,14},{-1,2,7,11,14},{1,2,3,7,11,14}}
00139 ]$
00140 uhit_def[5,15] : [
00141  max_var_hitting_def(5)[2],
00142  max_var_hittingdef2_cs(4)[2]
00143 ]$
00144 
00145 
00146 /* Deficiency 6 */
00147 
00148 uhit_def[6,"info"] : [false,4,inf,[[4,true],[5,unknown],[6,unknown],[19,unknown]]]$
00149 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def6.mac")$
00150 uhit_def[6,19] : [
00151  max_var_hitting_def(6)[2]
00152 ]$
00153 
00154 
00155 /* Deficiency 7 */
00156 
00157 uhit_def[7,"info"] : [false,4,inf,[[4,true],[5,unknown],[6,unknown],[23,unknown]]]$
00158 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def7.mac")$
00159 uhit_def[7,23] : [
00160  max_var_hitting_def(7)[2]
00161 ]$
00162 
00163 
00164 /* Deficiency 8 */
00165 
00166 uhit_def[8,"info"] : [false,4,inf,[[4,true],[5,unknown],[6,unknown],[27,unknown]]]$
00167 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def8.mac")$
00168 uhit_def[8,27] : [
00169  max_var_hitting_def(8)[2]
00170 ]$
00171 
00172 
00173 /* Deficiency 9 */
00174 
00175 uhit_def[9,"info"] : [false,4,inf,[[4,true],[5,unknown],[6,unknown],[31,unknown]]]$
00176 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def9.mac")$
00177 uhit_def[9,31] : [
00178  max_var_hitting_def(9)[2],
00179  max_var_hittingdef2_cs(5)[2]
00180 ]$
00181 
00182 
00183 /* Deficiency 10 */
00184 
00185 uhit_def[10,"info"] : [false,4,inf,[[4,true],[5,unknown],[6,unknown],[35,unknown]]]$
00186 
00187 uhit_def[10,4] : [
00188  {{-4,-3,-2},{-4,-3,-1,2},{-4,-3,1,2},{-4,-2,-1,3},{-4,-2,1,3},
00189   {-4,-1,2,3},{-3,-2,-1,4},{-3,-2,1,4},{-3,-1,2,4},{-3,1,2,4},
00190   {-2,-1,3,4},{-2,1,3,4},{-1,2,3,4},{1,2,3}},
00191  {{-4,-3,-2,-1},{-4,-3,-2,1},{-4,-3,-1,2},{-4,-2,-1,3},
00192   {-4,-2,1,3},{-4,-1,2,3},{-3,-2,-1,4},{-3,-2,1,4},{-3,-1,2,4},
00193   {-3,1,2},{-2,-1,3,4},{-2,1,3,4},{-1,2,3,4},{1,2,3}},
00194  {{-4,-3,-2,-1},{-4,-3,-1,2},{-4,-3,1},{-4,-2,-1,3},{-4,-2,1,3},
00195   {-4,-1,2,3},{-3,-2,-1,4},{-3,-2,1,4},{-3,-1,2,4},{-3,1,2,4},
00196   {-2,-1,3,4},{-2,1,3,4},{-1,2,3,4},{1,2,3}},
00197  {{-4,-3,-2,-1},{-4,-3,-1,2},{-4,-3,1,2},{-4,-2,-1,3},{-4,-2,1,3},
00198   {-4,-1,2,3},{-3,-2,-1,4},{-3,-2,1},{-3,-1,2,4},{-3,1,2,4},
00199   {-2,-1,3,4},{-2,1,3,4},{-1,2,3,4},{1,2,3}},
00200  {{-4,-3,-2,1},{-4,-3,-1,2},{-4,-3,1,2},{-4,-2,-1,3},{-4,-2,1,3},
00201   {-4,-1,2,3},{-3,-2,-1},{-3,-2,1,4},{-3,-1,2,4},{-3,1,2,4},
00202   {-2,-1,3,4},{-2,1,3,4},{-1,2,3,4},{1,2,3}}
00203 ]$
00204 uhit_def[10,5] : [
00205  {{-5,-4,-3,-1},{-5,-4,-3,1},{-5,-3,-1,4},{-5,-3,1,4},{-5,-2,3},{-4,-3,2,5},
00206   {-4,-2,-1,5},{-4,-2,1,5},{-4,-1,2,3},{-4,1,2,3},{-3,-1,4,5},{-3,1,4,5},
00207   {-2,3,4,5},{-1,2,3,4},{1,2,3,4}}
00208 ]$
00209 uhit_def[10,6] : [
00210  {{-6,-4,-1,3,5},{-6,-3,-2,1},{-6,-3,2,4},{-6,-2,-1,4,5},{-6,-1,2,3,4},
00211   {-6,1,3,5},{-5,-4,-1,2,3},{-5,-3,1,4,6},{-5,-2,-1},{-5,-1,2,4,6},{-5,1,3},
00212   {-4,-3,-2,-1,5},{-4,-3,-2,1,6},{-4,-3,2},{-4,3,5,6},{4,5,6}},
00213  {{-6,-5,-4,-2,-1},{-6,-5,-4,-2,1},{-6,-5,-3,2},{-6,-5,-2,-1,4},
00214   {-6,-5,-2,1,4},{-6,-2,3,5},{-5,-3,6},{-4,-3,-1,5},{-4,-3,1,5},{-4,-1,2,3},
00215   {-4,1,2,3},{-3,-1,4,5},{-3,1,4,5},{-2,3,6},{-1,2,3,4},{1,2,3,4}},
00216 {{-6,-3,-2,5},{-6,-2,3},{-5,-4,-3,-1},{-5,-4,-3,1},{-5,-3,-1,4},{-5,-3,1,4},
00217  {-5,-2,3,6},{-4,-2,5,6},{-4,-1,2,3},{-4,1,2,3},{-3,-1,2,5},{-3,1,2,5},
00218  {-2,-1,4,5,6},{-2,1,4,5,6},{-1,2,3,4},{1,2,3,4}},
00219 {{-6,-4,-3,5},{-6,-4,-2,3,5},{-6,-3,2,4},{-6,-2,4,5},{-5,-4,-1},{-5,-4,1},{-5,-3,2,4,6},
00220  {-5,-2,-1,4},{-5,-2,1,4},{-4,-1,2,3,5},{-4,1,2,3,5},{-3,-1,5,6},{-3,1,5,6},{-2,3,5,6},
00221  {-1,2,3,4},{1,2,3,4}},
00222 {{-6,-5,-3,-1},{-6,-5,-3,1},{-6,-5,-1,3},{-6,-5,1,3},{-6,-2,4,5},{-6,2,5},{-5,-4,-2,3,6},
00223  {-5,-3,-2,-1,6},{-5,-3,-2,1,6},{-4,-2,-1,5},{-4,-2,1,5},{-4,2,6},{-3,-2,4,5,6},{-3,2,4,6},
00224  {-1,3,4,6},{1,3,4,6}},
00225 {{-6,-5,-3,2},{-6,-4,-2,-1},{-6,-4,-2,1},{-6,-2,-1,4},{-6,-2,1,4},{-5,-3,6},{-5,-2,3,6},
00226  {-4,-2,5,6},{-4,-1,2,3},{-4,1,2,3},{-3,-1,2,5},{-3,1,2,5},{-2,-1,4,5,6},{-2,1,4,5,6},{-1,2,3,4},
00227  {1,2,3,4}},
00228 {{-6,-5,-4,3},{-6,-3,-1},{-6,-3,1},{-6,-2,3,4},{-5,-4,-1,6},{-5,-4,1,6},{-5,-2,-1,4,6},
00229  {-5,-2,1,4,6},{-4,-3,5,6},{-4,-2,3,5},{-4,-1,2,3,5},{-4,1,2,3,5},{-3,2,4,6},{-2,4,5,6},
00230  {-1,2,3,4},{1,2,3,4}},
00231 {{-6,-5,-4,-3,-1},{-6,-5,-4,-3,1},{-6,-5,-3,-1,4},{-6,-5,-3,1,4},{-6,-5,-2,3},{-6,-3,2,5},
00232  {-5,-4,-2,-1,6},{-5,-4,-2,1,6},{-5,-2,4,6},{-4,-1,2,3},{-4,1,2,3},{-3,2,6},{-2,-1,5},{-2,1,5},
00233  {-1,2,3,4},{1,2,3,4}},
00234 {{-6,-3,-2,5},{-6,-2,3,5},{-5,-4,-3,-1},{-5,-4,-3,1},{-5,-3,-1,4},{-5,-3,1,4},{-5,-2,-1,3},
00235  {-5,-2,1,3},{-4,-2,5,6},{-4,-1,2,3},{-4,1,2,3},{-3,-1,2,5},{-3,1,2,5},{-2,4,5,6},{-1,2,3,4},
00236  {1,2,3,4}},
00237 {{-6,-5,-4,-1},{-6,-5,-4,1},{-6,-4,-1,5},{-6,-4,1,5},{-6,-2,-1,4},{-6,-2,1,4},{-5,-1,2,3,4},
00238  {-5,1,2,3,4},{-4,-3,6},{-4,-2,3,6},{-4,-1,2,3,6},{-4,1,2,3,6},{-3,2,4},{-2,4,6},{-1,2,3,4,5},
00239  {1,2,3,4,5}}
00240 ]$
00241 uhit_def[10,35] : [
00242   max_var_hitting_def(10)[2]
00243 ]$
00244 
00245 
00246 /* Deficiency 11 */
00247 
00248 uhit_def[11,"info"] : [false,4,inf,[[4,true],[6,unknown]]]$
00249 
00250 uhit_def[11,4] : [nearly_full_hitting_fcs(4)[2]]$
00251 
00252 uhit_def[11,6] : [
00253 {{-6,-5,-3,2},{-6,-4,-2,-1},{-6,-4,-2,1},{-6,-2,-1,4},{-6,-2,1,4},
00254  {-5,-4,-3,-1,6},{-5,-4,-3,1,6},{-5,-3,-1,4,6},{-5,-3,1,4,6},{-4,-1,2,3},
00255  {-4,1,2,3},{-3,-2,5,6},{-3,-1,2,5},{-3,1,2,5},{-2,3,6},{-1,2,3,4},{1,2,3,4}},
00256 {{-6,-4,-3,-1},{-6,-4,-3,1},{-6,-3,-1,4},{-6,-3,1,4},{-6,-2,3},{-5,-3,2,6},{-5,-2,4,6},
00257  {-4,-3,2,5,6},{-4,-2,-1,6},{-4,-2,1,6},{-4,-1,2,3},{-4,1,2,3},{-3,-1,4,5,6},{-3,1,4,5,6},
00258  {-2,3,4,5,6},{-1,2,3,4},{1,2,3,4}}
00259 ]$
00260 
00261 /*
00262 uhit_def[11,39] : [
00263   max_var_hitting_def(11)[2]
00264 ]$
00265 */
00266 
00267 
00268 /* Deficiency 12 */
00269 
00270 uhit_def[12,"info"] : [false,4,inf,[[4,true],[5,unknown],[6,unknown],[7,false]]]$
00271 uhit_def[12,4] : [full_fcs(4)[2]]$
00272 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def12.mac")$
00273 uhit_def[12,7] : [
00274   rbrouwer1999[2]
00275 ]$
00276 /*
00277 uhit_def[12,43] : [
00278   max_var_hitting_def(12)[2]
00279 ]$
00280 */
00281 
00282 
00283 /* Deficiency 13 */
00284 
00285 uhit_def[13,"info"] : [false,5,inf,[[5,false]]]$
00286 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def13.mac")$
00287 /*
00288 uhit_def[13,47] : [
00289  max_var_hitting_def(13)[2]
00290 ]$
00291 */
00292 
00293 
00294 /* Deficiency 14 */
00295 
00296 uhit_def[14,"info"] : [false,5,inf,[[5,false]]]$
00297 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def14.mac")$
00298 /*
00299 uhit_def[14,51] : [
00300  max_var_hitting_def(14)[2]
00301 ]$
00302 */
00303 
00304 
00305 /* Deficiency 15 */
00306 
00307 uhit_def[15,"info"] : [false,5,inf,[[5,false],[7,unknown]]]$
00308 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def15.mac")$
00309 /*
00310 uhit_def[15,55] : [
00311  max_var_hitting_def(15)[2]
00312 ]$
00313 */
00314 
00315 
00316 /* Deficiency 16 */
00317 
00318 uhit_def[16,"info"] : [false,5,inf,[[5,false]]]$
00319 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def16.mac")$
00320 /*
00321 uhit_def[16,59] : [
00322  max_var_hitting_def(16)[2]
00323 ]$
00324 */
00325 
00326 
00327 /* Deficiency 17 */
00328 
00329 uhit_def[17,"info"] : [false,5,inf,[[5,false]]]$
00330 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def17.mac")$
00331 /*
00332 uhit_def[17,63] : [
00333  max_var_hitting_def(17)[2],
00334  max_var_hittingdef2_cs(6)[2]
00335 ]$
00336 */
00337 
00338 
00339 /* Deficiency 18 */
00340 
00341 uhit_def[18,"info"] : [false,5,inf,[[5,false]]]$
00342 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def18.mac")$
00343 /*
00344 uhit_def[18,67] : [
00345  max_var_hitting_def(18)[2]
00346 ]$
00347 */
00348 
00349 
00350 /* Deficiency 19 */
00351 
00352 uhit_def[19,"info"] : [false,5,inf,[[5,false]]]$
00353 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def19.mac")$
00354 /*
00355 uhit_def[19,71] : [
00356  max_var_hitting_def(19)[2]
00357 ]$
00358 */
00359 
00360 
00361 /* Deficiency 20 */
00362 
00363 uhit_def[20,"info"] : [false,5,inf,[[5,false]]]$
00364 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def20.mac")$
00365 /*
00366 uhit_def[20,75] : [
00367  max_var_hitting_def(20)[2]
00368 ]$
00369 */
00370 
00371 
00372 /* Deficiency 21 */
00373 
00374 uhit_def[21,"info"] : [false,5,inf,[[5,false]]]$
00375 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def21.mac")$
00376 /*
00377 uhit_def[21,79] : [
00378  max_var_hitting_def(21)[2]
00379 ]$
00380 */
00381 
00382 
00383 /* Deficiency 22 */
00384 
00385 uhit_def[22,"info"] : [false,5,inf,[[5,false]]]$
00386 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def22.mac")$
00387 /*
00388 uhit_def[22,83] : [
00389  max_var_hitting_def(22)[2]
00390 ]$
00391 */
00392 
00393 
00394 /* Deficiency 23 */
00395 
00396 uhit_def[23,"info"] : [false,5,inf,[[5,false]]]$
00397 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def23.mac")$
00398 /*
00399 uhit_def[23,87] : [
00400  max_var_hitting_def(23)[2]
00401 ]$
00402 */
00403 
00404 
00405 /* Deficiency 24 */
00406 
00407 uhit_def[24,"info"] : [false,5,inf,[[5,false],[8,false]]]$
00408 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def24.mac")$
00409 uhit_def[24,8] : [
00410   brouwer1999[2]
00411 ]$
00412 /*
00413 uhit_def[24,91] : [
00414   max_var_hitting_def(24)[2]
00415 ]$
00416 */
00417 
00418 
00419 /* Deficiency 25 */
00420 
00421 uhit_def[25,"info"] : [false,5,inf,[[5,false]]]$
00422 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def25.mac")$
00423 /*
00424 uhit_def[25,95] : [
00425  max_var_hitting_def(25)[2]
00426 ]$
00427 */
00428 
00429 
00430 /* Deficiency 26 */
00431 
00432 uhit_def[26,"info"] : [false,5,inf,[[5,true]]]$
00433 uhit_def[26,5] : [nearly_full_hitting_fcs(5)[2]]$
00434 /*
00435 uhit_def[26,99] : [
00436  max_var_hitting_def(26)[2]
00437 ]$
00438 */
00439 
00440 
00441 /* Deficiency 27 */
00442 
00443 uhit_def[27,"info"] : [false,5,inf,[[5,true]]]$
00444 uhit_def[27,5] : [full_fcs(5)[2]]$
00445 /*
00446 uhit_def[27,103] : [
00447  max_var_hitting_def(27)[2]
00448 ]$
00449 */
00450 
00451 /* Deficiency 28 */
00452 
00453 uhit_def[28,"info"] : [false,6,inf,[[6,false]]]$
00454 uhit_def[28,6] : [over_full_hitting_fcs(5)[2]]$
00455 
00456 
00457 /* Deficiency 43 */
00458 
00459 uhit_def[43,"info"] : [false,6,inf,[[6,false]]]$
00460 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def43.mac")$
00461 /*
00462 uhit_def[43,127] : [
00463  max_var_hitting_def(43)[2]
00464 ]$
00465 */
00466 
00467 /* Deficiency 58 */
00468 
00469 uhit_def[58,"info"] : [false,6,inf,[[6,true]]]$
00470 uhit_def[58,6] : [full_fcs(6)[2]]$
00471 /*
00472 uhit_def[58,227] : [
00473  max_var_hitting_def(58)[2]
00474 ]$
00475 */
00476 
00477 /* Deficiency 59 */
00478 
00479 uhit_def[59,"info"] : [false,7,inf,[[7,false]]]$
00480 uhit_def[59,7] : [over_full_hitting_fcs(6)[2]]$
00481 
00482 
00483 
00484 /* *************************************
00485    * Bounds on the deficiency and on n *
00486    *************************************
00487 */
00488 
00489 /* For given number of variables n, the maximal deficiency k
00490   such that an unsatisfiable hitting clause-set with these parameters
00491   exists. This unique clause-set is full_fcs(n)[2], which is non-singular
00492   for n <> 1. */
00493 max_def_uhit_n(n) := 2^n - n$
00494 
00495 /* For given deficiency k, the conjectured ([OK,XSZ, 2008]) minimal n
00496    for which unsatisfiable non-singular hitting clause-sets exist: */
00497 /* The smallest n with max_def_uhit_n(n) >= k. */
00498 /* Using the Lambert-function lambertW(z,x) from Mupad, this is
00499    ceil(-k - lambertW(-1, -exp(-k))).
00500 */
00501 min_n_uhit_def_i(k) := for n : 0 do if 2^n - n >= k then return(n)$
00502 /* Alternative computation using the Lambert-W-function. */
00503 /* This computation is much slower and also error-prone, but there might be
00504    some theoretical interest in it. */
00505 min_n_uhit_def_l(k) := if k=1 then 0 else
00506  ceiling(-k - lambert_w_b(-2^(-k), 2))$
00507 /* The branch "-1" of the Lambert-W-function: */
00508 lambert_w1(z):= block([eps :  bfloat(10^(-fpprec+1))],
00509  z : bfloat(z),
00510  block(
00511   [w1, w2 : 0, p : bfloat(-sqrt(2*%e*z+2))],
00512    w1 : bfloat(((((((-221/8505*p)+769/17280)*p-43/540)*p+11/72)*p-1/3)*p+1)*p-1),
00513    while w2 - w1 >= eps do (w2 : w1, w1 : bfloat(log(z/w1))),
00514    return(w1)))$
00515 /* Using this branch, the slightly generalised Lambert-W-function
00516    for base b (instead of e): */
00517 lambert_w_b(x,b) := block([fpprec : 20],
00518  bfloat(lambert_w1(log(b) * x) / log(b)))$
00519 
00520 
00521 /* ***************************
00522    * Accessing the catalogue *
00523    ***************************
00524 */
00525 
00526 /* The list of all clause-sets in the catalogue for a given deficiency k >= 1.
00527    Sorted by ascending number of variables, and for a given number of variables
00528    in the given order.
00529 */
00530 all_uhit_def(k) := block([L : uhit_def[k,"info"]],
00531   if op(L) = uhit_def then return([]),
00532   lappend(create_list(uhit_def[k,n],n,map(first,L[4]))))$
00533 
00534 
00535 /* Apply function f to all elements of the catalogue:
00536    Call f(k,n,i,F), store the results in a list. */
00537 apply_uhit(f) := block([list_def : uhit_def[0,"info"], result : []],
00538   for k in list_def do block([list_n : map(first,uhit_def[k,"info"][4])],
00539     for n in list_n do block([L : ev(uhit_def[k,n],eval)],
00540       for i : 1 thru length(L) do block([F : L[i]],
00541         result : endcons(f(k,n,i,F),result)))
00542   ),
00543   return(result))$
00544 
00545 
00546 /* Collecting all clause-sets (into a set) from the uhit-catalogue for a
00547    given number of variables and a range of deficiencies.
00548    Prerequisite: k0, k1, n >= 0 are natural numbers.
00549 */
00550 collect_uhit_n(n,k0,k1) :=
00551   setify(lappend(sublist(
00552     create_list(uhit_def[k,n],k,k0,k1),
00553     lambda([L], is(op(L) # uhit_def)))))$
00554 
00555 /* Extracting the triple [n_data, c_data, def_data] from the uhit-catalogue:
00556     - n_data is the sorted list of occurring numbers of variables
00557     - c_data is a list of the same length, with entries true/false stating
00558       whether it is guaranteed that the collection is complete for the
00559       corresponding n-value
00560     - def_data: a list of pairs, showing for each n-value the min- and max-
00561       deficiencies.
00562 */
00563 uhit_n_data() := block([D : uhit_def[0,"info"], h : sm2hm({}), res],
00564  for k in D do
00565   for p in uhit_def[k,"info"][4] do
00566     set_hm(h,first(p),cons([k,second(p)],ev_hm_d(h,first(p),[]))),
00567  set_hm(h,1,[]),
00568  res : listify(hm2sm(h)),
00569  [map(first,res),
00570   map(lambda([L], every(lambda([p],is(p[2]=true)),L)), map(second,res)),
00571   map(lambda([L], [lmin(map(first,L)),lmax(map(first,L))]), map(second,res))])$
00572 
00573 /* The set of all known non-singular unsatisfiable hitting
00574    clause-sets for a given number of variables:
00575     - uhit_n(-1,something) yields the list of available n-values
00576     - uhit_n(n,true) = true/false, depending on wether the list is complete or
00577       not (as c_data above)
00578     - uhit_n(n,false) is the set of available clause-sets.
00579 */
00580 uhit_n(n,info) := block([n_data, c_data, def_data],
00581  [n_data, c_data, def_data] : uhit_n_data(),
00582  if n = -1 then return(n_data)
00583  elseif not elementp(n,setify(n_data)) then
00584    if info then return(false) else return({})
00585  elseif info then return(c_data[n+1])
00586  else block([K : def_data[n+1]],
00587    if K=[inf,minf] then return({})
00588    else return(collect_uhit_n(n,K[1],K[2]))))$
00589 
00590 
00591 /* ****************************
00592    * Evaluating the catalogue *
00593    ****************************
00594 */
00595 
00596 /* For a list of candidate clause-sets, determine whether F is
00597    reduced unsatisfiable hitting, and in the positive case
00598    determine whether F is contained in the catalogue or not,
00599    where in the positive case the index-triple is returned.
00600    So for each F the corresponding entry in the return list
00601    is either false or [[k,n],i] or [[k,n],"new"].
00602 */
00603 classify_candidates_uhit_def(L) := block([result : []],
00604   for F in L do block([check : check_hitting_nsing_def(F)],
00605     if length(check) = 0 then result : endcons(false,result)
00606     else block([element : [check[1], nvar_cs(F)], catalist],
00607       catalist : uhit_def[element[1], element[2]],
00608       if not listp(catalist) then result : endcons([element,"new"],result)
00609       else block([found : false],
00610         for i : 1 thru length(catalist) unless found do
00611           if is_isomorphic_btr_cs(F, catalist[i]) then (
00612             found : true,
00613             result : endcons([element, i],result)
00614           ),
00615         if not found then result : endcons([element,"new"],result)
00616       )
00617     )
00618   ),
00619   return(result))$
00620 
00621 /* Similarly to analyse_isorepo_defset, but only keeps the clause-sets s.t.
00622    their min-var-degree is equal to the upper bound nonmersenne
00623    and which are not already in the uhit-catalogue. */
00624 /* Repository must be an isomorphism-type repository of unsatisfiable
00625    non-singular hitting clause-sets. */
00626 analyse_isorepo_defset_mvd(repository) := block(
00627  [M : hm2sm(repository), h : sm2hm({})],
00628   for P in M do block([def : P[1][2] - P[1][1], mvd],
00629     mvd : nonmersenne_rec[def],
00630     set_hm(h,def,union(ev_hm_d(h,def,{}),
00631       subset(map(fcs2cs,P[2]),
00632         lambda([F],is(min_variable_degree_cs(F)=mvd
00633           and classify_candidates_uhit_def([F])[1][2]="new")))))),
00634   sort(listify(hm2sm(h)),lambda([P1,P2], is(P1[1] < P2[1]))))$
00635 
00636 /* This variation keeps those clause-sets which improve the min-var-degrees
00637    per deficiency in the catalogue. */
00638 /* If the uhit-catalogue has been updated, then the memoised values of
00639    max_min_var_deg_uhit_def_mem might be wrong. */
00640 analyse_isorepo_defset_imprmvd(repository) := block(
00641  [M : hm2sm(repository), h : sm2hm({})],
00642   for P in M do block([def : P[1][2] - P[1][1], mvd],
00643     mvd : max_min_var_deg_uhit_def_mem[def],
00644     if mvd < nonmersenne_rec[def] then (
00645       set_hm(h,def,union(ev_hm_d(h,def,{}),
00646         subset(map(fcs2cs,P[2]),
00647           lambda([F],is(min_variable_degree_cs(F) > mvd))))))),
00648   sort(listify(hm2sm(h)),lambda([P1,P2], is(P1[1] < P2[1]))))$
00649 
00650 
00651 /* Compute the reduced isomorphism type of a clause-set F w.r.t.
00652    non-singular unsatisfiable hitting clause-sets:
00653     - [false] iff F is not unsatisfiable or not a hitting clause-set
00654       after singular DP-reduction
00655     - [[k,n],"new"] iff not in the catalogue
00656     - [[k,n],i] iff in the catalogue, with deficiency k, number of
00657       variables n and index i.
00658    According to [Kullmann, Zhao, 2012], for unsatisfiable hitting
00659    clause-sets F the result of sdp_reduction_cs(F) is unique.
00660 */
00661 redisotype_uhit_def(F) := classify_candidates_uhit_def(
00662   [sdp_reduction_cs(F)])[1]$
00663 
00664 
00665 /* ****************************
00666    * Completing the catalogue *
00667    ****************************
00668 */
00669 
00670 /* Closures under partial assignments
00671 
00672    First under all partial assigments:
00673 */
00674 
00675 /* For all clause-sets in the catalogue with number of variables at most
00676    n_bound, apply all partial assignments, followed by iterated elimination
00677    of singular variables, and compute the non-isomorphic cases found not to
00678    be in the catalogue, in the form of a repository of isomorphism types,
00679    which is passed by name. Returned is the number of new clause-sets
00680    found in this way. */
00681 closure_uhit_def_pass(n_bound, _hash_repo) := block(
00682  [min_n_unknown, /* the smallest n for which we don't have a
00683                          complete classification */
00684   count : 0],
00685   _hash_repo :: sm2hm({}),
00686   for n : 0 unless numberp(min_n_unknown) do
00687     if not uhit_n(n,true) then min_n_unknown : n,
00688   for n : min_n_unknown + 1 thru n_bound do
00689     for F in uhit_n(n,false) do
00690       for npass : 1 thru n - min_n_unknown do block([P : all_pass_n(setn(n),npass)],
00691         for phi in P do block(
00692          [G : sdp_reduction_cs(apply_pa(phi,F)), V],
00693           V : var_cs(G),
00694           if
00695             length(V) >= min_n_unknown and
00696              classify_candidates_uhit_def([G])[1][2] = "new" and
00697              manage_repository_isomorphism_types([V,G],ev(_hash_repo)) then
00698               count : count + 1
00699         )
00700       ),
00701   return(count))$
00702 /* Recall that via hm2osm(_hasp_repo) one gets the hash-map as list. */
00703 
00704 /* Now considering only elementary partial assignments: */
00705 
00706 /* For a nonsingular unsatisfiable hitting clause-set F consider all
00707    "nonsingular splittings", that is splitting on one variable followed
00708    by elimination of singular variables. The result is, as above, a
00709    repository of isomorphism types (those not already in uhit_def),
00710    which is passed by name, and the number of new clause-sets found (however,
00711    here _hash_repo is not reset: start an empty repository with
00712    _hash_repo:sm2hm({})):
00713 */
00714 nonsingular_splitting_uhit_def_cs(F, _hash_repo) := block(
00715  [V : var_cs(F), count : 0, G],
00716   for v in V do
00717    for x in [-v,+v] do (
00718      G : sdp_reduction_cs(apply_pa_cs({x},F)),
00719      if classify_candidates_uhit_def([G])[1][2] = "new" and
00720       manage_repository_isomorphism_types(cs2fcs(G),ev(_hash_repo)) then
00721        count : count + 1
00722    ),
00723   count)$
00724 
00725 /* Applying this elementary splitting for all elements in uhit_def up to
00726    deficiency k, now resetting the hash-repository:
00727 */
00728 closure_nonsingular_splitting_uhit(k, _hash_repo) := block([count : 0],
00729  _hash_repo :: sm2hm({}),
00730  for d : 2 thru k do
00731   for F in all_uhit_def(d) do
00732     count : count + nonsingular_splitting_uhit_def_cs(F, _hash_repo),
00733  count)$
00734 
00735 
00736 /* Closure under glueing */
00737 
00738 /* Computing the repository of isomorphism types not already in the
00739    uhit-cataloge for deficiency k, obtained by variable-disjoint full glueing
00740    of elements in the uhit-catalogue:
00741 */
00742 vardisjoint_glueing_uhit_def(k) := block([h:sm2hm({}), L1,k2,L2,FF],
00743  for k1 : 2 thru k-1 do (
00744    L1 : all_uhit_def(k1),
00745    k2 : k+1-k1,
00746    if k2 < k1 then return(done),
00747    L2 : all_uhit_def(k2),
00748    for F1 in L1 do
00749     for F2 in L2 do (
00750       FF : vardisjoint_full_gluing(cs2fcs(F1),cs2fcs(F2)),
00751       if classify_candidates_uhit_def([fcs2cs(FF)])[1][2] = "new" then
00752         manage_repository_isomorphism_types(FF,h)
00753     )
00754  ),
00755  h)$
00756 
00757 
00758 /* Closure under DP-resolution */
00759 
00760 /* Performing one step of DP-reduction for unsatisfiable hitting clause-set F,
00761    over all variables, followed by elimination of singular variables, and
00762    collect the results not already in uhit_def in the repository _hash_repo of
00763    isomorphism types (passed by name, not reset); returning the number of new
00764    isomorphism-types found:
00765 */
00766 nonsingular_DP_uhit_def_cs(F, _hash_repo) := block(
00767  [V : var_cs(F), count : 0, G],
00768   for v in V do (
00769     G : sdp_reduction_cs(dp_operator_cs(F,v)),
00770     if classify_candidates_uhit_def([G])[1][2] = "new" and
00771       manage_repository_isomorphism_types(cs2fcs(G),ev(_hash_repo)) then
00772       count : count + 1
00773   ),
00774   count)$
00775 
00776 /* Applying the "elementary" DP-reduction for all elements in uhit_def up to
00777    deficiency k, now resetting the hash-repository:
00778 */
00779 closure_nonsingular_DP_uhit(k, _hash_repo) := block([count : 0],
00780  _hash_repo :: sm2hm({}),
00781  for d : 2 thru k do
00782   for F in all_uhit_def(d) do
00783     count : count + nonsingular_DP_uhit_def_cs(F, _hash_repo),
00784  count)$
00785 
00786