OKlibrary  0.2.1.6
CardinalityConstraints.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 15.7.2009 (Swansea) */
00002 /* Copyright 2009, 2010, 2011 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 
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00029 
00030 
00031 /*
00032   A "(boolean) cardinality-constraint" ("crd") is a triple [a,L,b],
00033   where a, b are natural numbers >= 0 or inf, while L is a list of
00034   (boolean) literals (allowing repetitions and complementary literals).
00035   The meaning is "a <= sum(L) <= b", where sum(L) counts the satisfied
00036   literals.
00037 
00038   A crd is "repetition-free", if no literal in L occurs more than once.
00039 */
00040 
00041 /* ***************************************
00042    * Simplifying cardinality constraints *
00043    ***************************************
00044 */
00045 
00046 /*
00047   A "sorted cardinality constraint" ("scrd") is a triple [lb,C0,ub] similar
00048   to above, but where C0 now is an ordered set-map, sorted by descending
00049   values, which assigns to the occurring literals their counts (natural
00050   numbers >= 1).
00051 */
00052 
00053 /* Translating a cardinality constraint into a sorted cardinality constraint,
00054    sorting literals with equal counts in the build-in order:
00055 */
00056 crd2scrd(C) := [C[1], sort(list_distribution(C[2]), lambda([p1,p2], is(second(p1)>second(p2)))), C[3]]$
00057 
00058 /* Translating a sorted cardinality constraint into a cardinality constraint:
00059 */
00060 scrd2crd(C) :=
00061   [C[1],lappend(map(lambda([a],create_list(a[1],i,1,a[2])),C[2])),C[3]]$
00062 
00063 /* Removing tautologies from a sorted cardinality constraint.
00064    Returned is the equivalent sorted cardinality constraint, where for
00065    every clashing pair of literals the literal(s) attaining the min-count
00066    are removed, while the bounds are reduced by the min-count.
00067 */
00068 remove_tautologies_scrd(C) := block(
00069 [a : C[1], b : C[3], h : osm2hm(C[2]), NC],
00070  NC : map(
00071   lambda([P], block([cneg : ev_hm(h,-P[1])],
00072     if cneg=false then P
00073     else block([cpos : ev_hm(h,P[1])],
00074       if cpos=0 then 0
00075       else (
00076         set_hm(h,-P[1],0),
00077         [a,b] : [a,b] - cneg,
00078         if cpos=cneg then 0
00079         else [P[1],cpos-cneg]
00080       )))),
00081   C[2]),
00082  [a,delete(0,NC),b])$
00083 
00084 
00085 /* **********************
00086    * Direct translation *
00087    **********************
00088 */
00089 
00090 /* Translating a cardinality constraint into a CNF-clause-list (which has
00091    first the clauses for the lower bound, and then the clauses for the
00092    upper bound):
00093 */
00094 direct_crd2cl(C) := block([R : remove_tautologies_scrd(crd2scrd(C)), a, b, D],
00095  [a : R[1], D : R[2], b : R[3]],
00096   append(direct_crd2cl_ge(D, a), direct_crd2cl_lt(D, b+1)))$
00097 
00098 /*  Given a sorted cardinality constraint [0,D,ub-1] without tautological
00099     literal-pairs, compute the equivalent clause-list.
00100     The order of the clause-list is as follows:
00101  1. The major sorting is given by the order of D (regarding the literals).
00102  2. For a given literal x, first the clauses containing -x and then the clauses
00103     not containing the underlying variable are taken.
00104 */
00105 direct_crd2cl_lt(D,ub) := if ub <= 0 then [{}]
00106  elseif emptyp(D) then []
00107  else block([p : first(D), x, c, with_x, without_x],
00108   x : first(p),
00109   c : second(p),
00110   with_x : direct_crd2cl_lt(rest(D), ub-c),
00111   without_x : direct_crd2cl_lt(rest(D), ub),
00112   with_x : remove_elements(without_x,with_x),
00113   with_x : add_element_l(-x,with_x),
00114   append(with_x, without_x)
00115 )$
00116 
00117 /* Given a sorted cardinality constraint [lb,D,inf] without tautological
00118    literal-pairs, compute the equivalent clause-list: */
00119 direct_crd2cl_ge(D,lb) := if lb <= 0 then [] else
00120  block([s : sum_l(map(second,D))],
00121   if lb > s then [{}]
00122   else direct_crd2cl_lt(map(lambda([p], [-first(p),second(p)]),D), s-lb+1))$
00123 
00124 /* Translating a list of cardinality constraints into a list of
00125    CNF-clause-lists:
00126 */
00127 direct_crdl2cl(F) := lappend(map(direct_crd2cl,F))$
00128 
00129 /* Translating a formal clause-cardinality-list into a formal clause-list:
00130 */
00131 direct_fccrdl2fcl(FF) := [FF[1], append(FF[2], direct_crdl2cl(FF[3]))]$
00132 
00133 
00134 /* ************************
00135    * Using unary encoding *
00136    ************************
00137 */
00138 
00139 /*
00140    A "CNF representation of a cardinality constraint [a,L,b]" is a clause-set
00141    F with var(L) <= var(F), whose satisfying assignments restricted to var(L)
00142    are exactly those of the condition [a,L,b], and such that every satisfying
00143    assignment for [a,L,b] has exactly one extension to a satisfying assignment
00144    of F.
00145 */
00146 
00147 /* The representation below is from "Efficient CNF Encoding of Boolean
00148    Cardinality Constraints" by Olivier Bailleux and Yacine Boufkhad, CP 2003,
00149    LNCS 2833 (Springer), 2003, pages 108-122.
00150 */
00151 
00152 /* 
00153   Computing a CNF representation of cardinality constraint C according
00154   to [BB 2003]. The new variables are of the form vru(...), and come
00155   after the original variables in the list of variables.
00156   Prerequisites: C is repetition-free.
00157 */
00158 unary_bb_crd2fcl(C) := block(
00159   [C_n : scrd2crd(remove_tautologies_scrd(crd2scrd(C))),
00160    p,E,q,S,FF_T,FF_C],
00161   p : C_n[1], E : C_n[2], q : C_n[3],
00162   S : create_list(vru_var(1,length(E),i),i,1,length(E)),
00163   FF_T : unary_bb_totaliser_fcl(E,S),
00164   FF_C : unary_bb_comparator_fcl(S,p,q),
00165   return([FF_T[1],append(FF_T[2],FF_C[2])]))$
00166 
00167 /* New variables are "vru(a,b,i)". (variable recursive unary)
00168    where vru(a,b,i) is the i-th variable in list of variables
00169    representing the unary representation of the cardinality of
00170    [E[a],...,E[b]]. */
00171 kill(vru)$
00172 declare(vru, noun)$
00173 declare(vru, posfun)$
00174 vru_var(a,b,i) := nounify(vru)(a,b,i)$
00175 
00176 /* For a list E of "input" literals and a list S of "output" variables
00177    of the same length, compute a clause-list F equivalent to the condition
00178    that S is a "unary representation" of the count of 1's in E, that is, w.r.t.
00179    the given order in S, if a total assignment assigns k 1's to E, then
00180    the first k variables in S are true, and the remaining variables are false.
00181    S and E must be disjoint and must each contain distinct variables.
00182    Variables in F are those of E and S together with variables vru(...).
00183 */
00184 unary_bb_totaliser_fcl(E,S) := unary_bb_totaliser_r_fcl(E,S,1,length(E))$
00185 /* For a list E of "input" literals and a list S of "output" variables
00186    of the same length, compute a clause-list F equivalent to the condition
00187    that S is a "unary representation" of the count of 1's in E where E is
00188    assumed to be the sublist [E'[a],...,E'[b]] for some (possibly) larger
00189    E' .
00190    S and E must be disjoint and must each contain distinct variables.
00191    Variables in F are those of E and S together with variables vru(...).
00192    The point is that this function is used recursively, and so a and b
00193    are used to ensure new variables do not clash.
00194 */
00195 unary_bb_totaliser_r_fcl(E,S, a,b) := 
00196   if length(E) < 1 then [E,[]]
00197   else block(
00198      [subtree_a : [[],[]], subtree_b : [[],[]], m_a,m_b, level,
00199       cs :[],V_a,V_b,m:length(E)],
00200     /* work out CNFs for the two children of this node */
00201     m_a : floor(m / 2), m_b : (m - m_a),
00202     if m_a > 1 then (
00203       V_a : map(
00204         lambda([i],vru_var(a,ceiling((a+b)/2-1),i)),
00205         create_list(i,i,1,m_a)),
00206       subtree_a : unary_bb_totaliser_r_fcl(take_elements(m_a,E), V_a,
00207         a,ceiling((a+b)/2-1)))
00208     else 
00209       V_a : take_elements(m_a,E),
00210     if m_b > 1 then (
00211       V_b : map(
00212         lambda([i],vru_var(ceiling((a+b)/2-1)+1,b,i)),
00213         create_list(i,i,1,m_b)),
00214       subtree_b : unary_bb_totaliser_r_fcl(rest(E,m_a),V_b,
00215         ceiling((a+b)/2-1)+1,b))
00216     else 
00217       V_b : rest(E,m_a),
00218     /* generate clauses ensuring correct unary representation for this node */
00219     for alph : 0 thru m_a do
00220       for beta : 0 thru m_b do block([sigma : alph+beta],
00221         if sigma > 0 then
00222         cs : cons(union(
00223             if alph > 0 then {-V_a[alph]} else {},
00224             if beta > 0 then {-V_b[beta]} else {},
00225             {S[sigma]}), cs),
00226         if sigma < m then
00227         cs : cons(union(
00228             if alph < m_a then {V_a[alph+1]} else {},
00229             if beta < m_b then {V_b[beta+1]} else {},
00230             {-S[sigma+1]}),
00231           cs)
00232       ),
00233     return(
00234       [stable_unique(append(E,S,subtree_a[1],subtree_b[1])),
00235        append(subtree_a[2], subtree_b[2], cs)])
00236   )$
00237 
00238 
00239 /* For a list S of variables and natural numbers p, q, compute a clause-list F 
00240    whose satisfying assignments are those total assignments where the first
00241    p variables are set to true, and all variables from the (q+1)-th onwards 
00242    are set to false. The clause-list returned is thus the list of
00243    length(S) - (q-p) unit-clauses where the first p variables in S occur as
00244    the first p (positive) literals in unit-clauses and the last
00245    (length(S)-q+1) variables occur as negative literals in the later
00246    unit-clauses.
00247    Prerequisite: 0 <= p <= q, p and q are integers or inf.
00248 */
00249 unary_bb_comparator_fcl(S,p,q) :=
00250   if p > length(S) then [S,[{}]]
00251   else
00252     [S,append(
00253       map(set,take_elements(p,S)),
00254       map(set,map("-",rest(S,min(q,length(S))))))]$
00255 
00256