OKlibrary  0.2.1.6
GeneralisedUCP.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 31.1.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/Generators.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")\$
00026
00027 kill(f)\$
00028
00029 /* **********************
00030    * The r_k reductions *
00031    **********************
00032 */
00033
00034 okltest_generalised_ucp_cs(f) := block(
00035   for k : 0 thru 10 do (
00036     assert(f({},k) = {}),
00037     assert(f({{}},k) = {{}}),
00038     assert(f({{},{1,2}},k) = {{}}),
00039     assert(f({{1},{-1,2,3}},k) = if k=0 then {{1},{-1,2,3}} else {{2,3}}),
00040     assert(f({{1},{-1,2}},k) = if k=0 then {{1},{-1,2}} else {}),
00041     assert(f({{1,2},{3},{-3}},k) = if k=0 then {{1,2},{3},{-3}} else {{}})
00042   ),
00043   if oklib_test_level = 0 then return(true),
00044
00045   for k : 1 thru 3 do block([F : weak_php_cs(k+1,k)],
00046     for k2 : 0 thru k-1 do
00047       assert(f(F,k2) = F),
00048     assert(f(F,k) = {{}})
00049   ),
00050   if oklib_test_level = 1 then return(true),
00051
00052   for k : 4 thru 4 do block([F : weak_php_cs(k+1,k)],
00053     for k2 : 0 thru k-1 do
00054       assert(f(F,k2) = F),
00055     assert(f(F,k) = {{}})
00056   ),
00057   if oklib_test_level = 2 then return(true),
00058
00059   true
00060 )\$
00061
00062
00063 okltest_generalised_ucp_pa(f) := block(
00064   okltest_generalised_ucp_cs(buildq([f], lambda([F,k], f(F,k)[1]))),
00065
00066   for k : 0 thru 10 do (
00067     assert(f({},k)[2] = {}),
00068     assert(f({{}},k)[2] = {}),
00069     assert(apply_pa(f({{},{1,2}},k)[2], {{},{1,2}}) = {{}}),
00070     assert(f({{1},{-1,2,3}},k)[2] = if k=0 then {} else {1}),
00071     assert(f({{1},{-1,2}},k)[2] = if k=0 then {} else {1,2})
00072   ),
00073   if oklib_test_level = 0 then return(true),
00074
00075   for k : 1 thru 3 do block([F : weak_php_cs(k+1,k)],
00076     for k2 : 0 thru k-1 do
00077       assert(f(F,k2)[2] = {}),
00078     assert(apply_pa(f(F,k)[2], F) = {{}})
00079   ),
00080   if oklib_test_level = 1 then return(true),
00081
00082   for k : 4 thru 4 do block([F : weak_php_cs(k+1,k)],
00083     for k2 : 0 thru k-1 do
00084       assert(f(F,k2)[2] = {}),
00085     assert(apply_pa(f(F,k)[2], F) = {{}})
00086   ),
00087   if oklib_test_level = 2 then return(true),
00088
00089   true
00090 )\$
00091
00092 okltest_generalised_ucp_opa(f) := block([F],
00093   assert(okltest_generalised_ucp_pa(buildq([f],lambda([F,k], block([R:f(F,k)], [R[1],setify(R[2])])))) = true),
00094   for n : 1 thru 5 do (
00095     F : setify(rest(listify(smusat_horn_cs(n)))),
00096     for k : 0 thru 3 do
00097       if k = 0 then assert(f(F,k) = [F,[]])
00098       else assert(f(F,k) = [{},create_list(trv_var(create_list(2,j,1,i-1)),i,1,n)])
00099   ),
00100   F : {{1,2},{-1,2},{1,-2}},
00101   for k : 0 thru 4 do
00102     if k <= 1 then assert(f(F,k) = [F,[]])
00103     else assert(f(F,k) = [{},[1,2]]),
00104   for n : 0 thru 3 do (
00105     F : full_fcs(n)[2],
00106     for k : 0 thru 4 do
00107       assert(f(F,k) = if k < n then [F,[]]
00108       else [{{}},create_list(i,i,1,n)])
00109   ),
00110   /* XXX */
00111   true)\$
00112
00113
00114 /* *******************************
00115    * Reduction by weak autarkies *
00116    *******************************
00117 */
00118
00119 okltest_weakaut_red(f) := block([F],
00120   for k : 0 thru 5 do (
00121     assert(f({},k) = {}),
00122     assert(f({{}},k) = {{}}),
00123     assert(f({{1,2}},k) = if k=0 then {{1,2}} else {}),
00124     F : {{1,-2},{2,-3},{3,-4},{4}},
00125     assert(f(F,k) = if k=0 then F else {}),
00126     F : {{-1},{1},{2}},
00127     assert(f(F,k) = if k=0 then F else {{-1},{1}}),
00128     F : {{1,2},{-1,-2}},
00129     assert(f(F,k) = if k<=1 then F else {}),
00130     F : {{1,2},{-1,-2},{1,2,3},{1,2,-3}},
00131     assert(f(F,k) = if k=0 then F elseif k=1 then {{1,2},{-1,-2}}
00132       else {})
00133   ),
00134   if oklib_test_level = 0 then return(true),
00135   true)\$
00136
00137
00138 okltest_weakaut_red_pa(f) := block([F],
00139   okltest_weakaut_red(buildq([f],lambda([F,k],f(F,k)[1]))),
00140
00141   for k : 0 thru 5 do (
00142     assert(f({},k)[2] = {}),
00143     assert(f({{}},k)[2] = {}),
00144     F : {{1,2}},
00145     if k=0 then
00146       assert(f(F,k)[2] = {})
00147     else
00148       assert(apply_pa(f(F,k)[2], F) = {}),
00149     F : {{1,-2},{2,-3},{3,-4},{4}},
00150     if k=0 then
00151       assert(f(F,k)[2] = {})
00152     else
00153       assert(f(F,k)[2] = {1,2,3,4}),
00154     F : {{1,2},{-1,-2}},
00155     if k<=1 then
00156       assert(f(F,k)[2] = {})
00157     else
00158       assert(apply_pa(f(F,k)[2], F) = {})
00159   ),
00160   if oklib_test_level = 0 then return(true),
00161   true)\$
00162
00163
00164 /* ****************************************************************
00165    * Combining generalised unit-clause and weak-autarky-reduction *
00166    ****************************************************************
00167 */
00168
00169 okltest_generalised_ucp_war(f) := block([F],
00170   for k : 0 thru 10 do (
00171     assert(f({},k) = {}),
00172     assert(f({{}},k) = {{}}),
00173     assert(f({{},{1,2}},k) = {{}}),
00174     F : {{1},{-1,2,3}},
00175     assert(f(F,k) = if k=0 then F else {}),
00176     F : {{1,2},{-1,2},{1,-2}},
00177     assert(f(F,k) = if k<=1 then F else {})
00178   ),
00179   if oklib_test_level = 0 then return(true),
00180   true)\$
00181
00182 okltest_generalised_ucp_war_pa(f) := block(
00183   okltest_generalised_ucp_war(buildq([f],lambda([F,k],f(F,k)[1]))),
00184
00185   for k : 0 thru 10 do (
00186     assert(f({},k)[2] = {}),
00187     assert(f({{}},k)[2] = {}),
00188     F : {{},{1,2}},
00189     assert(apply_pa(f(F,k)[2],F) = {{}}),
00190     F : {{1},{-1,2,3}},
00191     if k=0 then
00192       assert(f(F,k)[2] = {})
00193     else
00194       assert(apply_pa(f(F,k)[2],F) = {}),
00195     F : {{1,2},{-1,2},{1,-2}},
00196     if k<=1 then
00197       assert(f(F,k)[2] = {})
00198     else
00199       assert(apply_pa(f(F,k)[2],F) = {})
00200   ),
00201   if oklib_test_level = 0 then return(true),
00202
00203   true)\$
00204
00205
00206 /* ******************************************************************
00207    * Generalised elimination of pure literals by forced assignments *
00208    ******************************************************************
00209 */
00210
00211 okltest_generalised_ple(f) := block([F],
00212   for k : 0 thru 5 do (
00213     assert(f({},k) = {}),
00214     assert(f({{}},k) = {{}}),
00215     assert(f({{1,2}},k) = {}),
00216     F : {{1,-2},{2,-3},{3,-4},{4}},
00217     assert(f(F,k) = {}),
00218     F : {{-1},{1},{2}},
00219     assert(f(F,k) = if k = 0 then {{-1},{1}} else F),
00220     F : {{1,2},{-1,-2}},
00221     assert(f(F,k) = if k=0 then F else {}),
00222     F : {{1,2},{-1,2},{1,-2},{-1,-2},{3,4},{-3,4},{-3,-4}},
00223     assert(f(F,k) = if k#1 then F else {{1,2},{-1,2},{1,-2},{-1,-2}})
00224   ),
00225   if oklib_test_level = 0 then return(true),
00226   true)\$
00227
00228 okltest_generalised_ple_pa(f) := block([F],
00229   okltest_generalised_ple(buildq([f],lambda([F,k],f(F,k)[1]))),
00230   for k : 0 thru 5 do (
00231     assert(f({},k)[2] = {}),
00232     assert(f({{}},k)[2] = {}),
00233     F : {{1,2}},
00234     assert(apply_pa(f(F,k)[2],F) = {}),
00235     F : {{1,-2},{2,-3},{3,-4},{4}},
00236     assert(apply_pa(f(F,k)[2],F) = {}),
00237     F : {{-1},{1},{2}},
00238     assert(f(F,k)[2] = if k = 0 then {2} else {}),
00239     F : {{1,2},{-1,-2}},
00240     if k=0 then
00241       assert(f(F,k)[2] = {})
00242     else
00243       assert(apply_pa(f(F,k)[2],F) = {}),
00244     F : {{1,2},{-1,2},{1,-2},{-1,-2},{3,4},{-3,4},{-3,-4}},
00245     if k#1 then
00246       assert(f(F,k)[2] = {})
00247     else
00248       assert(apply_pa(f(F,k)[2],F) = {{1,2},{-1,2},{1,-2},{-1,-2}})
00249   ),
00250   if oklib_test_level = 0 then return(true),
00251   true)\$
00252
00253
00254 /* *******************************************************
00255    * Look-ahead reduction for r_k and enforced autarkies *
00256    *******************************************************
00257 */
00258
00259 okltest_generalised_ucp_ple(f) := block([F],
00260   for k : 0 thru 5 do (
00261     assert(f({},k) = {}),
00262     assert(f({{}},k) = {{}}),
00263     assert(f({{1,2}},k) = {}),
00264     F : {{1,-2},{2,-3},{3,-4},{4}},
00265     assert(f(F,k) = {}),
00266     F : {{-1},{1},{2}},
00267     assert(f(F,k) = {{}}),
00268     F : {{1,2},{-1,-2}},
00269     assert(f(F,k) = if k=0 then F else {}),
00270     F : {{1,2},{-1,2},{1,-2},{-1,-2},{3,4},{-3,4},{-3,-4}},
00271     assert(f(F,k) = if k=0 then F else {{}})
00272   ),
00273   if oklib_test_level = 0 then return(true),
00274   true)\$
00275
00276 okltest_generalised_ucp_ple_pa(f) := block([F],
00277   okltest_generalised_ucp_ple(buildq([f],lambda([F,k],f(F,k)[1]))),
00278   for k : 0 thru 5 do (
00279     assert(f({},k)[2] = {}),
00280     assert(f({{}},k)[2] = {}),
00281     F : {{1,2}},
00282     assert(apply_pa(f({{1,2}},k)[2],F) = {}),
00283     F : {{1,-2},{2,-3},{3,-4},{4}},
00284     assert(f(F,k)[2] = {1,2,3,4}),
00285     F : {{-1},{1},{2}},
00286     assert(apply_pa(f(F,k)[2],F) = {{}}),
00287     F : {{1,2},{-1,-2}},
00288     if k=0 then
00289       assert(f(F,k)[2] = {})
00290     else
00291       assert(apply_pa(f(F,k)[2],F) = {}),
00292     F : {{1,2},{-1,2},{1,-2},{-1,-2},{3,4},{-3,4},{-3,-4}},
00293     if k=0 then
00294       assert(f(F,k)[2] = {})
00295     else
00296       assert(apply_pa(f(F,k)[2],F) = {{}})
00297   ),
00298   if oklib_test_level = 0 then return(true),
00299   true)\$
00300
00301
```