OKlibrary  0.2.1.6
CardinalityConstraints.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 16.7.2009 (Swansea) */
00002 /* Copyright 2009, 2010 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 
00041 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00042 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac")$
00043 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/UnitClausePropagation.mac")$
00044 
00045 kill(f)$
00046 
00047 
00048 /* ***************************************
00049    * Simplifying cardinality constraints *
00050    ***************************************
00051 */
00052 
00053 okltest_crd2scrd(f) := block([a,b],
00054   assert(f([a,[],b]) =  [a,[],b]),
00055   assert(f([a,[1,2,-1,-2,1,3,2],b]) = [a, [[1,2],[2,2],[-2,1],[-1,1],[3,1]], b]),
00056   true)$
00057 
00058 okltest_scrd2crd(f) := block([a,b],
00059   assert(f([a,[],b]) =  [a,[],b]),
00060   assert(f([a, [[1,2],[2,2],[-2,1],[-1,1],[3,1]], b]) =
00061     [a,[1,1,2,2,-2,-1,3],b]),
00062   true)$
00063 
00064 okltest_remove_tautologies_scrd(f) := block([a,b],
00065   assert(f([a,[],b]) = [a,[],b]),
00066   assert(f([a,[[1,1]],b]) = [a,[[1,1]],b]),
00067   assert(f([a,[[1,1]],b]) = [a,[[1,1]],b]),
00068   assert(f([a,[[1,1],[-1,1]],b]) = [a-1,[],b-1]),
00069   assert(f([a,[[1,2],[-1,1]],b]) = [a-1,[[1,1]],b-1]),
00070   assert(f([a,[[-1,2],[1,1]],b]) = [a-1,[[-1,1]],b-1]),
00071   assert(f([a,[[1,3],[2,2],[-1,2],[-2,2],[3,1]],b]) = [a-4,[[1,1],[3,1]],b-4]),
00072   true)$
00073 
00074 
00075 /* **********************
00076    * Direct translation *
00077    **********************
00078 */
00079 
00080 okltest_direct_crd2cl(f) := (
00081   assert(f([0,[1,-1],0]) = [{}]),
00082   assert(f([0,[1,-1],1]) = []),
00083   assert(f([1,[1,-1],1]) = []),
00084   assert(f([2,[1,-1],inf]) = [{}]),
00085   assert(f([2,[1,-1,1],2]) = [{1}]),
00086   assert(f([2,[1,-1,1],inf]) = [{1}]),
00087   assert(f([2,[1,-1,1,-1],2]) = []),
00088   assert(f([2,[1,-1,1,-1,3],2]) = [{-3}]),
00089   assert(f([0,[1,-1,1,-1,3,3,-3],2]) = [{}]),
00090   assert(f([3,[1,-1,1,-1,3,3,-3],3]) = [{-3}]),
00091   /* XXX */
00092   true)$
00093 
00094 okltest_direct_crd2cl_lt(f) := (
00095   for ub : -1 thru 1 do
00096     assert(f([],ub) = if ub <= 0 then [{}] else []),
00097   for c : 1 thru 3 do
00098     for ub : -1 thru c+3 do
00099       assert(f([[1,c]], ub) = if ub<=0 then [{}] elseif ub<=c then [{-1}] else []),
00100   assert(f([[1,1],[2,1]],0) = [{}]),
00101   assert(f([[1,1],[2,1]],1) = [{-1},{-2}]),
00102   assert(f([[1,1],[2,1]],2) = [{-1,-2}]),
00103   assert(f([[1,1],[2,1]],3) = []),
00104   assert(f([[1,2],[2,1]],1) = [{-1},{-2}]),
00105   assert(f([[1,2],[2,1]],2) = [{-1}]),
00106   assert(f([[1,2],[2,1]],3) = [{-1,-2}]),
00107   assert(f([[1,1],[2,2]],1) = [{-1},{-2}]),
00108   assert(f([[1,1],[2,2]],2) = [{-2}]),
00109   assert(f([[1,1],[2,2]],3) = [{-1,-2}]),
00110   assert(f([[1,2],[2,2]],2) = [{-1},{-2}]),
00111   assert(f([[1,2],[2,2]],3) = [{-1,-2}]),
00112   assert(f([[1,2],[2,2]],4) = [{-1,-2}]),
00113   assert(f([[1,2],[2,2]],5) = []),
00114   /* XXX */
00115   true)$
00116 
00117 okltest_direct_crd2cl_ge(f) := (
00118   assert(f([],0) = []),
00119   assert(f([],1) = [{}]),
00120   assert(f([[1,1]],0) = []),
00121   assert(f([[1,1]],1) = [{1}]),
00122   assert(f([[1,1]],2) = [{}]),
00123   assert(f([[1,3]],0) = []),
00124   assert(f([[1,3]],1) = [{1}]),
00125   assert(f([[1,3]],2) = [{1}]),
00126   assert(f([[1,3]],3) = [{1}]),
00127   assert(f([[1,3]],4) = [{}]),
00128   assert(f([[1,1],[-2,2]], 1) = [{1,-2}]),
00129   assert(f([[1,1],[-2,2]], 2) = [{-2}]),
00130   assert(f([[1,1],[-2,2]], 3) = [{1},{-2}]),
00131   assert(f([[1,1],[-2,2]], 4) = [{}]),
00132   /* XXX */
00133   true)$
00134 
00135 
00136 /* ************************
00137    * Using unary encoding *
00138    ************************
00139 */
00140 
00141 okltest_unary_bb_totaliser_fcl(f) := block([F],
00142   assert(f([],[]) = [[],[]]),
00143   assert(f([2],[1]) = [[2,1],[{-2,1},{-1,2}]]),
00144   assert(f([3,4],[1,2]) =
00145     [[3,4,1,2],[{-4,-3,2},{-2,4},{-3,1},{-2,3},{-4,1},{-1,3,4}]]),
00146   assert(f([4,5,6],[1,2,3]) =
00147     [[4,5,6,1,2,3,vru(2,3,1),vru(2,3,2)],
00148      [{-6,-5,vru(2,3,2)},{6,-vru(2,3,2)},{-5,vru(2,3,1)},{5,-vru(2,3,2)},
00149       {-6,vru(2,3,1)},{5,6,-vru(2,3,1)},{-4,3,-vru(2,3,2)},{-3,vru(2,3,2)},
00150       {-4,2,-vru(2,3,1)},{-2,vru(2,3,1)},{-4,1},{-3,4},{2,-vru(2,3,2)},
00151       {-2,4,vru(2,3,2)},{1,-vru(2,3,1)},{-1,4,vru(2,3,1)}]]),
00152   /* XXX */
00153   true)$
00154 
00155 okltest_unary_bb_totaliser_r_fcl(f) := block(
00156   okltest_unary_bb_totaliser_fcl_comb(
00157     buildq([f],lambda([E,S], f(E,S,1,length(E))))),
00158   
00159   true)$
00160 
00161 okltest_unary_bb_comparator_fcl(f) := block(
00162   for m : 0 thru 5 do
00163     for n : 0 thru 5 do (
00164       assert(f([],0,0) = [[],[]]),
00165       assert(f([],0,inf) = [[],[]]),
00166       assert(f([],inf,0) = [[],[{}]])),
00167   assert(f([1],0,1) = [[1],[]]),
00168   assert(f([1],inf,1) = [[1],[{}]]),
00169   assert(f([1],0,inf) = [[1],[]]),
00170   assert(f([1],1,1) = [[1],[{1}]]),
00171   assert(f([1,2,3],1,2) = [[1,2,3],[{1},{-3}]]),
00172   assert(f([1,2,3,4,5],2,4) = [[1,2,3,4,5],[{1},{2},{-5}]]),
00173   assert(f([1,2,3,4,5],2,inf) = [[1,2,3,4,5],[{1},{2}]]),
00174   true)$
00175 
00176 okltest_unary_bb_crd2fcl(f) := block([F],
00177   for m : 0 thru 5 do
00178     for n : 0 thru 5 do (
00179       assert(f([0,[],0]) = [[],[]]),
00180       assert(f([inf,[],0]) = [[],[{}]]),
00181       assert(f([0,[],inf]) = [[],[]])),
00182   assert(f([0,[1],1]) = [[1,vru(1,1,1)],[{-1,vru(1,1,1)},{1,-vru(1,1,1)}]]),
00183   assert(f([inf,[1],1]) =
00184     [[1,vru(1,1,1)],[{-1,vru(1,1,1)},{1,-vru(1,1,1)},{}]]),
00185   assert(f([0,[1],inf]) = [[1,vru(1,1,1)],[{-1,vru(1,1,1)},{1,-vru(1,1,1)}]]),
00186   assert(f([1,[1],1]) =
00187     [[1,vru(1,1,1)],[{-1,vru(1,1,1)},{1,-vru(1,1,1)},{vru(1,1,1)}]]),
00188   assert(f([1,[-1,1],2]) = f([0,[],1])),
00189   assert(f([1,[-1,1,2],2]) = f([0,[2],1])),
00190   true)$
00191 
00192