OKlibrary  0.2.1.6
Pigeonhole.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 26.8.2011 (Swansea) */
00002 /* Copyright 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 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac");
00028 
00029 kill(f)$
00030 
00031 
00032 /* ***********************
00033    * Pigeonhole formulas *
00034    ***********************
00035 */
00036 
00037 okltest_var_php_l(f) := (
00038   assert(f(0,0) = []),
00039   assert(f(0,1) = []),
00040   assert(f(1,0) = []),
00041   assert(f(1,1) = [php(1,1)]),
00042   assert(f(2,1) = [php(1,1),php(2,1)]),
00043   assert(f(1,2) = [php(1,1),php(1,2)]),
00044   assert(f(4,3) = [php(1,1),php(1,2),php(1,3),php(2,1),php(2,2),php(2,3),php(3,1),php(3,2),php(3,3),php(4,1),php(4,2),php(4,3)]),
00045   true)$
00046 
00047 okltest_pigeons_different_holes_cl(f) := (
00048   assert(f(0,0) = []),
00049   assert(f(0,1) = []),
00050   assert(f(1,0) = []),
00051   assert(f(1,1) = []),
00052   assert(f(1,2) = []),
00053   assert(f(2,1) = [{-php(1,1),-php(2,1)}]),
00054   assert(f(2,2) = [{-php(1,1),-php(2,1)},{-php(1,2),-php(2,2)}]),
00055   assert(f(2,3) = [{-php(1,1),-php(2,1)},{-php(1,2),-php(2,2)},{-php(1,3),-php(2,3)}]),
00056   assert(f(3,2) = [{-php(1,1),-php(2,1)},{-php(1,1),-php(3,1)},{-php(2,1),-php(3,1)},{-php(1,2),-php(2,2)},{-php(1,2),-php(3,2)},{-php(2,2),-php(3,2)}]),
00057   true)$
00058 
00059 okltest_pigeons_in_holes_cl(f) := (
00060   assert(f(0,0) = []),
00061   assert(f(0,1) = []),
00062   assert(f(1,0) = [{}]),
00063   assert(f(1,1) = [{php(1,1)}]),
00064   assert(f(1,2) = [{php(1,1),php(1,2)}]),
00065   assert(f(2,1) = [{php(1,1)},{php(2,1)}]),
00066   assert(f(2,2) = [{php(1,1),php(1,2)},{php(2,1),php(2,2)}]),
00067   assert(f(2,3) = [{php(1,1),php(1,2),php(1,3)},{php(2,1),php(2,2),php(2,3)}]),
00068   assert(f(3,2) = [{php(1,1),php(1,2)},{php(2,1),php(2,2)},{php(3,1),php(3,2)}]),
00069   true)$
00070 
00071 /* Measures */
00072 
00073 okltest_nvar_php(f) := block(
00074  for m : 0 thru 6 do
00075   for n : 0 thru 6 do
00076    assert(f(m,n) = nvar_fcs(weak_php_fcs(m,n))),
00077  true)$
00078 
00079 okltest_ncl_list_weak_php(f) := block(
00080  for m : 0 thru 6 do
00081   for n : 0 thru 6 do
00082    assert(f(m,n) = ncl_list_fcs(weak_php_fcs(m,n))),
00083  true
00084 )$
00085 
00086 okltest_ncl_weak_php(f) := block(
00087  for m : 0 thru 6 do
00088   for n : 0 thru 6 do
00089    assert(f(m,n) = ncl_fcs(weak_php_fcs(m,n))),
00090  true
00091 )$
00092 
00093 okltest_deficiency_weak_php(f) := block(
00094  for m : 0 thru 6 do
00095   for n : 0 thru 6 do
00096    assert(f(m,n) = deficiency_fcs(weak_php_fcs(m,n))),
00097  true
00098 )$
00099 
00100 
00101 /* *********************************
00102    * Extended pigeon-hole formulas *
00103    *********************************
00104 */
00105 
00106 
00107 okltest_php_induction_step_cl(f) := block(
00108   for i in [0] do
00109       assert(f(i) = []),
00110   assert(f(1) =
00111     [{php_ext(1,1,1),-php_ext(2,1,1)},{php_ext(1,1,1),-php_ext(2,1,2),
00112      -php_ext(2,3,1)},{-php_ext(1,1,1),php_ext(2,1,1),php_ext(2,1,2)},
00113      {-php_ext(1,1,1),php_ext(2,1,1),php_ext(2,3,1)},{php_ext(1,2,1),
00114      -php_ext(2,2,1)},{php_ext(1,2,1),-php_ext(2,2,2),-php_ext(2,3,1)},
00115      {-php_ext(1,2,1),php_ext(2,2,1),php_ext(2,2,2)},{-php_ext(1,2,1),
00116      php_ext(2,2,1),php_ext(2,3,1)}]),
00117   true)$
00118 
00119 okltest_php_induction_cl(f) := block(
00120   for i in [0,1] do
00121     assert(f(i) = []),
00122   assert(f(2) =
00123     [{php_ext(1,1,1),-php(1,1)},{php_ext(1,1,1),-php(1,2),-php(3,1)},
00124      {-php_ext(1,1,1),php(1,1),php(1,2)},{-php_ext(1,1,1),php(1,1),php(3,1)},
00125      {php_ext(1,2,1),-php(2,1)},{php_ext(1,2,1),-php(2,2),-php(3,1)},
00126      {-php_ext(1,2,1),php(2,1),php(2,2)},{-php_ext(1,2,1),php(2,1),php(3,1)}]),
00127   for i : 1 thru 3 do
00128     blocked_extension_cs_p(setify(f(i+1)),setify(f(i))),
00129   if oklib_test_level = 0 then return(true),
00130   for i : 4 thru 5 do
00131     blocked_extension_cs_p(setify(f(i+1)),setify(f(i))),
00132   true)$
00133 
00134 okltest_weak_php_unsat_ext_uni_fcs(f) := block(
00135   assert(
00136     okltest_weak_php_unsat_ext_fcs(
00137       buildq([f], lambda([m],
00138           cs2fcs(
00139             substitute_cl(f(m)[2], sm2hm(var_ephp2php_sm(m)))))))),
00140   true)$
00141 
00142 okltest_weak_php_unsat_ext_fcs(f) := block(
00143   for i in [0,1] do
00144     assert(f(i) = weak_php_fcs(i+1,i)),
00145   assert(f(2) =
00146     [{php(1,1),php(1,2),php(2,1),php_ext(1,1,1),php(2,2),php_ext(1,2,1),
00147       php(3,1),php(3,2)},
00148      {{-php(1,1),-php(2,1)},{-php(1,1),php_ext(1,1,1)},{-php(1,1),-php(3,1)},
00149       {php(1,1),php(1,2)},{php(1,1),php(1,2),-php_ext(1,1,1)},
00150       {php(1,1),-php_ext(1,1,1),php(3,1)},{-php(1,2),php_ext(1,1,1),-php(3,1)},
00151       {-php(1,2),-php(2,2)},{-php(1,2),-php(3,2)},{-php(2,1),php_ext(1,2,1)},
00152       {-php(2,1),-php(3,1)},{php(2,1),php(2,2)},{php(2,1),php(2,2),
00153        -php_ext(1,2,1)}, {php(2,1),-php_ext(1,2,1),php(3,1)},{-php(2,2),
00154        php_ext(1,2,1),-php(3,1)},{-php(2,2),-php(3,2)},{php(3,1),php(3,2)}}]),
00155   for m : 1 thru 3 do
00156     assert(blocked_extension_cs_p(f(m)[2], weak_php_cs(m+1,m))),
00157   if oklib_test_level = 0 then return(true),
00158   for m : 4 thru 5 do
00159     assert(blocked_extension_cs_p(f(m)[2], weak_php_cs(m+1,m))),
00160   true)$
00161 
00162 okltest_standardise_weak_php_unsat_ext_uni(f) := block(
00163   for m : 1 thru 10 do
00164     assert(
00165       create_list(f(m)(php_ext_var(l,i,j)), l, 1, m, i, 1, l+1, j, 1,l) =
00166       create_list(i, i, 1, f(m)(php_ext_var(m,m+1,m)))),
00167   true)$
00168 
00169 okltest_invstandardise_weak_php_unsat_ext_uni(f) := block(
00170   for m : 1 thru 4 do (
00171     assert(
00172       create_list(f(m)(i),
00173         i, 1, standardise_weak_php_unsat_ext_uni(m)(php_ext_var(m,m+1,m))) =
00174       create_list(php_ext_var(l,i,j), l, 1, m, i, 1, l+1, j, 1,l))),
00175   if oklib_test_level = 0 then return(true),
00176   for m : 5 thru 20 do (
00177     assert(
00178       create_list(f(m)(i),
00179         i, 1, standardise_weak_php_unsat_ext_uni(m)(php_ext_var(m,m+1,m))) =
00180       create_list(php_ext_var(l,i,j), l, 1, m, i, 1, l+1, j, 1,l))),
00181   if oklib_test_level = 1 then return(true),
00182   for m : 21 thru 40 do (
00183     assert(
00184       create_list(f(m)(i),
00185         i, 1, standardise_weak_php_unsat_ext_uni(m)(php_ext_var(m,m+1,m))) =
00186       create_list(php_ext_var(l,i,j), l, 1, m, i, 1, l+1, j, 1,l))),
00187   true)$
00188 
00189 okltest_weak_php_unsat_ext_stdfcs(f) := block(
00190   for i in [0,1] do
00191     assert(f(i) = standardise_fcs(weak_php_fcs(i+1,i))[1]),
00192   assert(f(2)=
00193     [{1,2,3,4,5,6,7,8},
00194        {{-8,-6},{-8,-4},{-7,-6,2},{-7,-5},{-7,-4,1},{-7,-3},{-6,-4},
00195         {-5,-3},{-5,2},{-3,1},{-2,5,6},{-2,5,7},{-1,3,4},{-1,3,7},
00196         {3,4},{5,6},{7,8}}]),
00197   true)$
00198 
00199 okltest_var_php2ephp_sm(f) := block(
00200   assert(f(0) = {}),
00201   true)$
00202 
00203 okltest_var_ephp2php_sm(f) := block(
00204   assert(f(0) = {}),
00205   true)$
00206 
00207 okltest_nvar_weak_php_unsat_ext(f) := block(
00208   assert(f(1) = 2),
00209   for i : 2 thru 4 do
00210     assert(f(i) = length(weak_php_unsat_ext_fcs(i)[1])),
00211   if oklib_level = 0 then return(true),
00212   for i : 5 thru 7 do
00213     assert(f(i) = length(weak_php_unsat_ext_fcs(i)[1])),
00214   true)$
00215 
00216 okltest_ncl_weak_php_unsat_ext(f) := block(
00217   assert(f(1) = 3),
00218   for i : 2 thru 4 do
00219     assert(f(i) = length(weak_php_unsat_ext_fcs(i)[2])),
00220   if oklib_level = 0 then return(true),
00221   for i : 5 thru 7 do
00222     assert(f(i) = length(weak_php_unsat_ext_fcs(i)[2])),
00223   true)$
00224 
00225