OKlibrary  0.2.1.6
SplittingTrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.1.2008 (Swansea) */
00002 /* Copyright 2008, 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/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/SplittingTrees.mac")$
00028 
00029 kill(f)$
00030 
00031 
00032 /* ***************************"""""""""
00033    * The notion of a "splitting tree" *
00034    ************************************
00035 */
00036 
00037 okltest_fst_p(f) := (
00038   assert(f(0) = false),
00039   assert(f([]) = false),
00040   assert(f([[]]) = true),
00041   assert(f([true]) = true),
00042   assert(f([false]) = true),
00043   assert(f([0]) = false),
00044   assert(f([0,[[]]]) = false),
00045   assert(f([0,[[]],[[]]]) = true),
00046   assert(f([0,[1],[[]]]) = false),
00047   assert(f([0,[1,[[]],[[]]],[[]]]) = true),
00048   assert(f([0,[1,[false],[true]],[false]]) = true),
00049   assert(f([0,[1,[false],[true]],[false],[[]]]) = false),
00050   true)$
00051 
00052 okltest_st_p(f) := (
00053   assert(f([[]],{}) = true),
00054   assert(f([true],{}) = true),
00055   assert(f([false],{}) = false),
00056   assert(f([[]],{{}}) = true),
00057   assert(f([true],{{}}) = false),
00058   assert(f([false],{{}}) = true),
00059   assert(f([[]],{{1}}) = true),
00060   assert(f([false],{{1}}) = false),
00061   assert(f([true],{{1}}) = false),
00062   assert(f([2,[[]],[[]]],{{1}}) = false),
00063   assert(f([1,[[]],[[]]],{{1}}) = true),
00064   assert(f([1,[true],[[]]],{{1}}) = false),
00065   assert(f([1,[false],[[]]],{{1}}) = true),
00066   assert(f([1,[false],[false]],{{1}}) = false),
00067   assert(f([1,[false],[true]],{{1}}) = true),
00068   assert(f([1,[false],[false]],{{1},{}}) = false),
00069   assert(f([1,[2,[[]],[[]]],[2,[[]],[[]]]], {{1,2},{1,-2}}) = false),
00070   assert(f([1,[2,[[]],[[]]],[[]]], {{1,2},{1,-2}}) = true),
00071   assert(f([1,[2,[[]],[[]]],[false]], {{1,2},{1,-2}}) = false),
00072   assert(f([1,[2,[[]],[[]]],[true]], {{1,2},{1,-2}}) = true),
00073   assert(f([1,[2,[false],[[]]],[2,[[]],[[]]]], {{1,2}, {3}}) = true),
00074   true)$
00075 
00076 okltest_est_p(f) := (
00077   assert(f([[]],{}) = true),
00078   assert(f([true],{}) = true),
00079   assert(f([false],{}) = false),
00080   assert(f([[]],{{}}) = true),
00081   assert(f([true],{{}}) = false),
00082   assert(f([false],{{}}) = true),
00083   assert(f([[]],{{1}}) = true),
00084   assert(f([false],{{1}}) = false),
00085   assert(f([true],{{1}}) = false),
00086   assert(f([2,[[]],[[]]],{{1}}) = true),
00087   assert(f([2,[true],[[]]],{{1}}) = false),
00088   assert(f([2,[[]],[false]],{{1}}) = false),
00089   assert(f([1,[[]],[[]]],{{1}}) = true),
00090   assert(f([1,[true],[[]]],{{1}}) = false),
00091   assert(f([1,[false],[[]]],{{1}}) = true),
00092   assert(f([1,[false],[false]],{{1}}) = false),
00093   assert(f([1,[false],[true]],{{1}}) = true),
00094   assert(f([1,[false],[false]],{{1},{}}) = true),
00095   assert(f([1,[2,[[]],[[]]],[2,[[]],[[]]]], {{1,2},{1,-2}}) = true),
00096   assert(f([1,[2,[[]],[[]]],[[]]], {{1,2},{1,-2}}) = true),
00097   assert(f([1,[2,[[]],[[]]],[false]], {{1,2},{1,-2}}) = false),
00098   assert(f([1,[2,[[]],[[]]],[true]], {{1,2},{1,-2}}) = true),
00099   assert(f([1,[2,[false],[false]],[true]], {{1,2},{1,-2}}) = true),
00100   assert(f([1,[2,[3,[[]],[false]],[false]],[true]], {{1,2},{1,-2}}) = true),
00101   assert(f([1,[2,[3,[true],[false]],[false]],[true]], {{1,2},{1,-2}}) = false),
00102   assert(f([1,[2,[3,[false],[false]],[false]],[true]], {{1,2},{1,-2}}) = true),
00103   true)$
00104 
00105 okltest_complete_stp(f) := (
00106   assert(f([[]]) = false),
00107   assert(f([false]) = true),
00108   assert(f([true]) = true),
00109   assert(f([1,[[]],[false]]) = false),
00110   assert(f([1,[true],[false]]) = true),
00111   true)$
00112 
00113 
00114 /* ********************************
00115    * Manipulating splitting trees *
00116    ********************************
00117 */
00118 
00119 okltest_fst2st(f) := (
00120   assert(f([1,[true],[true]],{{}}) = [false]),
00121   assert(f([1,[2,[3,[false],[false]],[false]],[true]], {{1,2},{1,-2}}) = [1,[2,[false],[false]],[true]]),
00122   assert(f([1,[2,[false],[[]]],[2,[[]],[[]]]], {{1,2}, {3}}) = [1,[2,[false],[[]]],[[]]]),
00123   /* XXX */
00124   true)$
00125 
00126 okltest_negate_st(f) := block(
00127   assert(f([true]) = [false]),
00128   assert(f([false]) = [true]),
00129   true)$
00130 
00131 okltest_condense_st(f) := block(
00132   assert(f([true]) = [true]),
00133   assert(f([false]) = [false]),
00134   assert(f([1,[false],[false]]) = [false]),
00135   assert(f([1,[false],[true]]) = [1,[false],[true]]),
00136   assert(f([1,[true],[false]]) = [1,[true],[false]]),
00137   assert(f([1,[true],[true]]) = [true]),
00138   assert(f([1,[2,[false],[false]],[2,[true],[true]]]) = [1,[false],[true]]),
00139   assert(f([1,[2,[false],[false]],[2,[false],[false]]]) = [false]),
00140   true)$
00141 
00142 /* ***************************
00143    * Finding splitting trees *
00144    ***************************
00145 */
00146 
00147 okltest_optimal_splitting_tree(f) := block(
00148   assert(f({}) = [[true],1]),
00149   assert(f({{}}) = [[false],1]),
00150   assert(f({{1}}) = [[1,[false],[true]],3]),
00151   assert(f({{1},{-1}}) = [[1,[false],[false]],3]),
00152   assert(f({{1},{2},{-1,-2}})[2] = 5),
00153   assert(f({{1},{2},{-1,-2},{}}) = [[false],1]),
00154   for n : 0 thru 4 do
00155     assert(f(full_fcs(n)[2])[2] = 2^(n+1)-1),
00156   if oklib_test_level = 0 then return(true),
00157   true)$
00158 
00159 okltest_optimal_r_splitting_tree(f) := block(
00160   okltest_optimal_splitting_tree(buildq([f],lambda([F],f(F,0)))),
00161   for k : 1 thru 5 do (
00162     assert(f({},k) = [[true],1]),
00163     assert(f({{}},k) = [[false],1]),
00164     assert(f({{1}},k) = [[true],1]),
00165     assert(f({{1},{-1}},k) = [[false],1])),
00166   if oklib_test_level = 0 then return(true),
00167   for k : 1 thru 3 do
00168     assert(f(weak_php_cs(k+1,k),k-1)[2] = if k=1 then 5 else 3),
00169   if oklib_test_level = 1 then return(true),
00170   for k : 4 thru 4 do
00171     assert(f(weak_php_cs(k+1,k),k-1)[2] = if k=1 then 5 else 3),
00172   true)$
00173 
00174 
00175 /* ******************************
00176    * Evaluating splitting trees *
00177    ******************************
00178 */
00179 
00180 okltest_sat_pass_st(f) := block(
00181   assert(f([true]) = [{}]),
00182   assert(f([false]) = []),
00183   assert(f([1,[false],[false]]) = []),
00184   assert(f([1,[true],[false]]) = [{-1}]),
00185   assert(f([1,[true],[true]]) = [{-1},{1}]),
00186   if oklib_test_level = 0 then return(true),
00187   block([oklib_test_level : min(oklib_test_level - 1, 2)],
00188     okltest_usat_clauses_st(buildq([f],lambda([T], comp_cs(f(negate_st(T))))))
00189   ),
00190   true)$
00191 
00192 okltest_usat_clauses_st(f) := block(
00193   assert(f([false]) = [{}]),
00194   assert(f([true]) = []),
00195   assert(f([1,[false],[false]]) = [{1},{-1}]),
00196   assert(f([1,[true],[false]]) = [{-1}]),
00197   assert(f([1,[true],[true]]) = []),
00198   if oklib_test_level = 0 then return(true),
00199   block([oklib_test_level : min(oklib_test_level - 1, 2)],
00200     okltest_sat_pass_st(buildq([f],lambda([T], comp_cs(f(negate_st(T))))))
00201   ),
00202   true)$
00203 
00204 okltest_st2reslrt_cs(f) := (
00205   assert(f([false],{{}}) = [{}]),
00206   assert(f([1,[false],[false]],{{1},{-1}}) = [{},[{1}],[{-1}]]),
00207   assert(f([-1,[false],[false]],{{1},{-1}}) = [{},[{-1}],[{1}]]),
00208   assert(f([1,[false],[2,[false],[false]]],{{1},{-1,2},{-1,-2}}) = [{},[{1}],[{-1},[{-1,2}],[{-1,-2}]]]),
00209   assert(f([1,[false],[false]],{{}}) = [{}]),
00210   /* XXX */
00211   true)$
00212 
00213 okltest_reslrt2st(f) := (
00214   assert(f([{}]) = [false]),
00215   assert(f([{},[{1}],[{-1}]]) = [1,[false],[false]]),
00216   assert(f([{},[{1}],[{-1},[{-1,2}],[{-1,-2}]]]) = [1,[false],[2,[false],[false]]]),
00217   /* XXX */
00218   true)$
00219 
00220 okltest_treepruning_st(f) := (
00221   assert(f([1,[false],[false]],{{}}) = [false]),
00222   assert(f([false],{{},{1},{-1}}) = [false]),
00223   assert(f([1,[false],[false]],{{},{1},{-1}}) = [false]),
00224   assert(f([2,[false],[false]],{{},{1},{-1}}) = [false]),
00225   /* XXX */
00226   true)$
00227 
00228 
00229 /* ***********************************
00230    * Generators for splitting trees  *
00231    ***********************************
00232 */
00233 
00234 okltest_complete_st_alldifferent(f) := (
00235   assert(f(0) = [false]),
00236   assert(f(1) = [trv([]),[false],[false]]),
00237   assert(f(2) = [trv([]),[trv([1]),[false],[false]],[trv([2]),[false],[false]]]),
00238   assert(f(3) = [trv([]),[trv([1]),[trv([1,1]),[false],[false]],[trv([1,2]),[false],[false]]],[trv([2]),[trv([2,1]),[false],[false]],[trv([2,2]),[false],[false]]]]),
00239   true)$
00240 
00241 okltest_horn_st(f) := (
00242   assert(f(0) = [false]),
00243   assert(f(1) = [trv([]), [false], [false]]),
00244   assert(f(2) = [trv([]), [false], [trv([2]),[false],[false]]]),
00245   assert(f(3) = [trv([]), [false], [trv([2]),[false],[trv([2,2]),[false],[false]]]]),
00246   true)$
00247 
00248 okltest_input_list_st(f) := (
00249   assert(f([],1) = 1),
00250   assert(okltest_horn_st(buildq([f], lambda([k], f(create_list(trv_var(create_list(2,j,1,i-1)), i,1,k), [false])))) = true),
00251   true)$
00252 
00253 okltest_genhorn_st(f) := block([x],
00254   assert(f(0,x) = [false]),
00255   assert(f(x,0) = [false]),
00256   assert(f(0,2) = [false]),
00257   assert(f(1,2) = [trv([]),[false],[false]]),
00258   assert(f(2,2) = [trv([]), [trv([1]),[false],[false]], [trv([2]),[false],[false]]]),
00259   for k : 0 thru 8 do
00260     assert(f(k,k) = complete_st_alldifferent(k)),
00261   true)$
00262 
00263 okltest_genhornsat_st(f) := (
00264   assert(f(0,x) = [trv([]),[false],[true]]),
00265   assert(f(x,0) = [trv([]),[false],[true]]),
00266   assert(f(0,2) = [trv([]),[false],[true]]),
00267   assert(f(1,2) = [trv([]),[trv([1]),[false],[true]],[trv([2]),[false],[true]]]),
00268   assert(f(2,2) = [trv([]), [trv([1]),[trv([1,1]),[false],[true]],[trv([1,2]),[false],[true]]], [trv([2]),[trv([2,1]),[false],[true]],[trv([2,2]),[false],[true]]]]),
00269   true)$
00270 
00271 
00272 /* ***********************
00273    * r_k splitting trees *
00274    ***********************
00275 */
00276 
00277 okltest_rst2st(f) := (
00278   /* XXX */
00279   true)$
00280 
00281 okltest_rst2est(f) := block([F],
00282   assert(f({{}},[false],0) = [false]),
00283   assert(f({{}},[false],1) = [false]),
00284   /* assert(f({{}},[false],2) = [false]), */
00285   assert(f({{1},{-1}},[1,[false],[false]],0) = [1,[false],[false]]),
00286   assert(f({{1},{-1}},[false],1) = [1,[false],[false]]),
00287   for k : 0 thru cokltl(7,40) do block([F : smusat_horn_stdfcs(k)[2]],
00288     assert(f(F,[false],1) = input_list_st(create_list(i,i,1,k), [false]))
00289   ),
00290   F : weak_php_cs(3,2),
00291   assert(f(F, [-php(1,1),[false],[false]], 1) = [-php(1,1),
00292        [-php(2,1),[false],[-php(3,1),[false],[php(2,2),[false],[php(3,2),[false],[false]]]]],
00293        [php(1,2),[false],[-php(2,2),[false],[-php(3,2),[false],[php(2,1),[false],[php(3,1),[false],[false]]]]]]]),
00294   true)$
00295 
00296 
00297 /* **********
00298    * Output *
00299    **********
00300 */
00301