OKlibrary  0.2.1.6
CardinalityConstraints.hpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 16.7.2009 (Swansea)
00002 /* Copyright 2009, 2010, 2011, 2012 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 
00331    \endverbatim
00332    b could also be defined as ceiling(n/2). </li>
00333    <li> Next we provide additional labels, namely the variables used at the
00334    leaves for input, the auxiliary variables used at inner non-root nodes for
00335    the unary representation, and the list of output variables at the root.
00336    </li>
00337    <li> n is then implicitly given as the (coinciding) lengths of the lists
00338    of input and output variables. </li>
00339    <li> An important aspect of the unary addition to be performed via binary
00340    splitting (as outlined via unary_addition_tree_0_lrt) is, that always
00341    literals with indices from an interval [a,b] are added, where for the
00342    root we have a=1 and b=n, while for the leaves we have a=b=i for 1 <= i <=
00343    n. </li>
00344    <li> This is presented by the following tree:
00345    \verbatim
00346 unary_addition_tree_1_lrt(n) := unary_addition_tree_1r_lrt(1,n)$
00347 /* Prerequisite: a, b natural numbers, a <= b */
00348 unary_addition_tree_1r_lrt(a,b) := if a=b then [a] else
00349  block([d : floor((b-a+1)/2)],
00350   [[a,b], 
00351    unary_addition_tree_1r_lrt(a,a+d-1), unary_addition_tree_1r_lrt(a+d,b)])$
00352 
00353 draw_lrt_dbl(unary_addition_tree_1_lrt(5));
00354 /* draw_lrt(unary_addition_tree_1_lrt(5),d:inf); */
00355    \endverbatim
00356    </li>
00357    <li> For T = unary_addition_tree_1_lrt(n), the leaves have labels i
00358    corresponding to input-literal i, while inner nodes have labels [a,b],
00359    corresponding to auxiliary variables vru(a,b,1), ..., vru(a,b,b-a+1). </li>
00360    <li> So the tree showing the literals and auxiliary variables used is as
00361    follows, where L is an arbitrary list of literals:
00362    \verbatim
00363 unary_addition_tree_2_lrt(L) := unary_addition_tree_2r_lrt(L,1,length(L))$
00364 unary_addition_tree_2r_lrt(L,a,b) := block([l : b-a+1],
00365  if l = 1 then L else
00366  block([d : floor(l/2)],
00367   [create_list(vru_var(a,b,i),i,1,l),
00368    unary_addition_tree_2r_lrt(take_elements(d,L),a,a+d-1),
00369    unary_addition_tree_2r_lrt(rest(L,d),a+d,b)]))$
00370 
00371 draw_lrt_dbl(unary_addition_tree_2_lrt([a,b,c,d,e]));
00372 /* draw_lrt(unary_addition_tree_2_lrt(5),d:inf); */
00373    \endverbatim
00374    </li>
00375    <li> Now only the function for the clause-set describing the relation
00376    between a non-leaf %node and its two children is needed, and then the
00377    totaliser-function is obtained by traversing the tree. </li>
00378    <li> This relation is that of unary addition. </li>
00379    <li> In the case of [BB 2003], unary addition of a list of literals A
00380    and B with output variables C is encoded by the formal clause-list
00381    generated by the following function
00382    \verbatim
00383 unary_bb_add_fcl(A,B,C) := block([F:[]],
00384     for alpha : 0 thru length(A) do
00385       for beta : 0 thru length(B) do block([sigma : alpha+beta],
00386         if sigma > 0 then
00387           F : cons(union(
00388               if alpha > 0 then {-A[alpha]} else {},
00389               if beta > 0 then {-B[beta]} else {},
00390               {C[sigma]}), F),
00391           if sigma < length(C) then
00392           F : cons(union(
00393               if alpha < length(A) then {A[alpha+1]} else {},
00394               if beta < length(B) then {B[beta+1]} else {},
00395               {-C[sigma+1]}),F)
00396           ),
00397     return([stable_unique(map(var_l,append(A,B,C))),F]))$
00398    \endverbatim
00399    </li>
00400    <li> See
00401    Experimentation/Investigations/BooleanFunctions/plans/UnaryAddition.hpp
00402    for investigations (there might be better choices than in the paper). </li>
00403   </ul>
00404 
00405 
00406   \todo Add statistics functions
00407   <ul>
00408    <li> These statistics functions rely on precise (combinatorial)
00409    specifications. </li>
00410   </ul>
00411    
00412 
00413   \todo Docus
00414   <ul>
00415    <li> DONE (these texts have been moved here)
00416    The current amount of text one finds in
00417    ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac
00418    is inappropriate --- function specifications should be rather short and
00419    succinct. </li>
00420    <li> If appropriate, these texts should be moved to the docus. </li>
00421    <li> So this text has a place only in the docus:
00422    \verbatim
00423    A CNF representation of a boolean cardinality constraint [a,L,b] with
00424    "detection of forced assignments via UCP" is a CNF representation of [a,L,b]
00425    with the property that for every partial assignment phi with
00426    var(phi) <= var(L) and every forced assignment <v -> e> for apply_pa(phi,F)
00427    with v in var(L), applying unit-clause-propagation to apply_pa(phi,F)
00428    includes this forced assignment (i.e., UCP derives all forced assignments
00429    for apply_pa(phi,F) which concern the cardinality constraint).
00430    \endverbatim
00431    </li>
00432    <li> And so does this text:
00433    \verbatim
00434    The following algorithm, from the above mentioned paper, computes a CNF
00435    representation F of the cardinality constraint [a,L,b] with detection of
00436    forced assignments via UCP.
00437 
00438    The algorithm takes as input a list E of literals, and then introduces
00439    a list of new (distinct) variables S of the same size as E, which under any
00440    assignment will have the unary representation (ones/trues appearing from
00441    the left) of the cardinality of E. The remainder of the algorithm consists
00442    of two phases, the totalizer and the comparator, and the clauses
00443    generated (and variables introduced) by these phases are then appended
00444    together to produce the final clause-set. The totalizer enforces that
00445    S is the unary representation of the cardinality of L and the comparator
00446    enforces that this unary representation represents a number in the range
00447    a to b.
00448 
00449    The totalizer takes as input a list E of input variables, and as
00450    output a list S of cardinality variables, and returns a list of
00451    clauses that enforce that S is a unary representation of E. This
00452    is done in a recursive manner, through the introduction of new variables,
00453    and clauses enforcing unary addition.
00454    
00455    In the totalizer, E is split into two sublists E_1 and E_2, where E_1 is
00456    the list of the first floor(length(E)/2) elements and E_2 is the remainder
00457    of E. The algorithm then introduces two lists of new (distinct) variables
00458    S_1 and S_2, where S_1 and S_2 are the same size as E_1 and E_2
00459    respectively. Totalizer is then run again for each of these sublists E_1
00460    with S_1 and E_2 with S_2 returning (new) variable and clause-lists V_1,C_1
00461    and V_2,C_2 respectively, and then the following clauses (C_3) are
00462    generated to enforce that in any satisfying assignment of F, we have that S
00463    is the unary addition of S_1 and S_2:
00464 
00465 
00466      for every 
00467        0 <= a <= length(E_1) and 
00468        0 <= b <= length(E_2) and
00469        0 <= c <= length(L) such that
00470        a + b = c we add the clauses
00471 
00472          1) {-S_1[a],-S_2[b],S[c]} and
00473    2) {S_1[a+1], S_2[b+1], S[c+1]}
00474 
00475    where (1) ensures (S_1[a] and S_2[b]) => S[a+b]), i.e., the unary
00476    addition holds in one direction and (2) ensures
00477    (S[a+b+1] => (S_1[a+1] or S_2[b+1]), i.e., the other direction, and we have
00478        
00479      S_1[0] = S_2[0] = S[0] = 1 and 
00480      S_1[length(E_1)+1] = S_2[length(E_2)+1] = S[length(L)+1] = 0
00481 
00482    for the extreme cases for the above clauses.
00483 
00484    In the base case where length(E) = 1, totalizer takes S_1 = E_1, and
00485    S_2 = E2, since E_1 and E_2 are their own unary representations.
00486 
00487    The comparator generates a list of unit-clauses
00488 
00489        [{S[1]},...,{S[a]},{S[b+1]},...,{S[length(L)]}]
00490 
00491    which ensures that, given that the totalizer ensures that S is the unary
00492    representation of the cardinality of E, any satisfying assignment
00493    which results in E having a cardinality less than a, or greater than b, 
00494    is a falsifying assignment for F.
00495 
00496    To use this algorithm see unary_bb_crd2fcl.
00497    \endverbatim
00498    </li>
00499    <li> Also the explanations for unary_bb_totaliser_fcl are misplaced:
00500    \verbatim
00501    The list of new variables introduced by this function can therefore be 
00502    recursively defined using a function vc, where
00503    V = rest(vc(E,1,length(E)), length(E)):
00504 
00505    vc(E,a,b) = [] if a == b
00506              else append(
00507                E, 
00508                vc([vru(a,ceiling((a+b)/2-1),1),...,
00509                    vru(a,ceiling((a+b)/2-1),floor(length(E)/2))],
00510                  a,floor((a+b)/2)),
00511                vc([vru(ceiling((a+b)/2-1)+1,b,1),...,
00512                  vru(ceiling((a+b)/2-1)+1,ceiling(length(E)/2))],
00513                  ceiling((a+b)/2-1)+1,b))
00514 
00515    Therefore the number of new variables introduced given length(E) = n is
00516    nvc(n) - n where nvc is defined recursively in the following way:
00517 
00518    nvc(n) = 0 if n < 1
00519             n + nvc(floor(n/2)) + nvc(ceiling(n/2)) otherwise
00520 
00521    Assuming S is without complimentary literals, a partial assignment phi
00522    satisfies F iff phi is total and given n is the cardinality of E under phi,
00523    we have that
00524 
00525      phi(S[i]) = 1 for 1 <= i <= n and phi(S[i]) = 0 for i > n,
00526 
00527    and given m is the cardinality of E[1,...,floor(length(E)/2)] we have
00528 
00529      phi(vru(1,floor(length(E)/2),i)) = 1 for 1 <= i <= m and
00530      phi(vru(1,floor(length(E)/2),i)) = 0 otherwise
00531 
00532    and given m' is the cardinality of E[floor(length(E)/2)+1,...,length(E)]
00533    we have
00534    
00535      phi(vru(floor(length(E)/2)+1,length(E),i)) = 1 for 1 <= i <= m' and
00536      phi(vru(floor(length(E)/2)+1,length(E),i)) = 0 otherwise
00537 
00538    and for all a and b such that we have a new variable vru(a,b,i) for some i,
00539    if b-a = 2 then we have
00540 
00541      phi(vru(a,b,1)) = phi(E[a]) xor phi(E[b])
00542      phi(vru(a,b,2)) = phi(E[a]) and phi(E[b])
00543 
00544    if b-a = 3 then we have
00545 
00546      phi(vru(a,b,1)) = phi(E[a]) or phi(vru(a+1,b,1))
00547      phi(vru(a,b,2)) = (phi(E[a]) and phi(vru(a+1,b,1))) or phi(vru(a+1,b,2))
00548      phi(vru(a,b,3)) = phi(E[a]) and phi(vru(a+1,b,2))
00549 
00550    and if b-a > 3 then we have
00551 
00552      phi(vru(a,b,i)) =
00553        there exist j,k such that j+k=i
00554          phi(vru(a,ceiling(a+b/2-1),j)) and phi(vru(ceiling(a+b/2-1)+1,b,k))
00555 
00556    i.e., in each case [vru(a,b,1),...,vru(a,b,b-a+1)] is the
00557    representation of the unary addition of E[a] and E[b], E[a] and
00558    [vru(a+1,b,1),vru(a+1,b,2)] or [vru(a,b',1),...,vru(a,b',b'-a+1)] and
00559    [vru(b'+1,b,1),...,vru(b'+1,b,b-b')] respectively depending on
00560    a and b, where b' = ceiling((a+b)/2-1).
00561 
00562    unary_bb_totalizer_r_fcl is a function with additional parameters
00563    to keep track of any new variables introduced, and has the same
00564    specification as unary_bb_totaliser_fcl, except
00565    V = rest(vc(E,a,b), length(E)).
00566    \endverbatim
00567    </li>
00568   </ul>
00569 
00570 
00571   \todo Implement adder-circuit translation
00572   <ul>
00573    <li> Also provide the translation using the Tseitin translation of
00574    the boolean adder circuits. </li>
00575    <li> See Satisfiability/Transformers/Generators/plans/LinInequal.hpp for 
00576    a C++ implementation. </li>
00577    <li> Joost Warners dissertation also describes such a translation; are
00578    there differences? </li>
00579   </ul>
00580 
00581 
00582   \todo Cardinality constraints as active clauses
00583   <ul>
00584    <li> As a special case of "Pseudo-boolean constraints as active clauses"
00585    (see ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/plans/general.hpp),
00586    cardinality constraints should yield a very attractive first model of
00587    "active clauses". </li>
00588    <li> Their interface as a set of clauses is given by their prime implicates
00589    representation (see "Direct realisations" below). </li>
00590   </ul>
00591 
00592 
00593   \todo Implement other methods using unary representation
00594   <ul>
00595    <li> [Een, Soerensson, 2006, Translating Pseudo-Boolean Constraints into
00596    SAT] contains another translation. </li>
00597    <li> And so does [Sinz, 2005, Towards an Optimal Encoding of Boolean
00598    Cardinality Constraints]. </li>
00599    <li> The newest article is [Asin et al, SAT 2009, Cardinality networks and
00600    their applications]. Perhaps this should be the starting point. </li>
00601    <li> In [Bailleux et al, SAT 2009, New encodings for pseudo-boolean
00602    constraints into CNF] one finds further remarks regarding the unary
00603    encoding. </li>
00604   </ul>
00605 
00606 
00607   \todo DONE Rename functions related to unary encoding
00608   <ul>
00609    <li> These functions realise only special implementations, and so a generic
00610    name like "cardinality_cl" is inappropriate. </li>
00611    <li> We should also use English spelling, for example "totaliser". </li>
00612    <li> "cardinality_cl" should become "unary_bb_crdl2fcl". </li>
00613   </ul>
00614 
00615 
00616   \todo DONE Functions such as cardinality_totalizer_cl should take cardinality
00617   constraints
00618   <ul>
00619    <li> Currently functions such as cardinality_totalizer_cl and
00620    cardinality_comparator_cl take the parameters given in the
00621    boolean constraint [a,L,b] individually. </li>
00622    <li> These functions should take the whole constraint as a single argument
00623    as in other functions such as crd2cl. </li>
00624   </ul>
00625 
00626 
00627   \todo DONE Provide complete specifications (related to unary encoding)
00628   <ul>
00629    <li> This relates to the algorithm implemented by MG according to
00630    [Bailleux, Boufkhad, 2003]. </li>
00631    <li> For cardinality_totalizer_cs, cardinality_comparator_cs and
00632    cardinality_cl *combinatorial* specifications are needed.
00633     <ol>
00634      <li> Currently there are no specifications (which, of course, must
00635      allow to reconstruct the clause-sets(!)). </li>
00636      <li> Some properties are mentioned in
00637      ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac,
00638      but these properties shouldn't be there (but possibly in the docus). </li>
00639     </ol>
00640    </li>
00641    <li> Then two levels of tests are needed: One which checks the
00642    (precise) combinatorial specification, and another one which checks
00643    the (general) specification as a presentation of some constraint.
00644     <ol>
00645      <li> Currently the tests are not specified at all. </li>
00646      <li> Of course, first the basic functions need to be specified. </li>
00647     </ol>
00648    </li>
00649    <li> This todo has been replaced by
00650     <ul>
00651      <li> "Partial assignments for CNFs with detection of forced assignments 
00652      via UCP" </li>
00653      <li> "Ordering for CNFs with detection of forced assignments via UCP" 
00654      </li>
00655     </ul>
00656    </li>
00657    <li> DONE Especially precise information on the added auxiliary variables are
00658    needed. </li>
00659   </ul>
00660 
00661 
00662   \bug DONE Nonsensical documentation
00663   <ul>
00664    <li> In
00665    ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac
00666    two large blocks of text are (exactly??) identical. </li>
00667    <li> This makes no sense. </li>
00668    <li> OK started to update the documentation, and the requests posed by OK
00669    should be answered as soon as possible (both in
00670    ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac
00671    and in
00672    ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/tests/CardinalityConstraints.mac
00673    . </li>
00674    <li> Also all the bad repetitions need to be removed. </li>
00675    <li> See 
00676     <ul>
00677      <li> "Partial assignments for CNFs with detection of forced assignments 
00678      via UCP" </li>
00679      <li> "Ordering for CNFs with detection of forced assignments via UCP" 
00680      </li>
00681     </ul>
00682    </li>
00683   </ul>
00684 
00685 
00686   \todo DONE Change specification of variables in cardinality_cl etc.
00687   <ul>
00688    <li> Currently the variables in cardinality_totalizer_cl, 
00689    cardinality_totalizer_cl etc are of the form "ctt(l,i)" where
00690    l is a list specifying where in the recursive procedure these variables
00691    are introduced. </li>
00692    <li> This representation relies heavily on the algorithm, and means
00693    that it is essentially impossible to properly define or describe the
00694    variables separately from the algorithm. </li>
00695    <li> However, these variables are simply the unary representation of
00696    the cardinality of a certain sublist L' of the list of input literals L, and
00697    therefore a better representation would be "ctt(a,b,i)" where a and b 
00698    define the upper and lower bound of the L' in L. </li>
00699    <li> Then for example, the initial variables list passed into
00700    cardinality_totalizer_cl as S, would be 
00701    [ctt(1,length(E),1),...,ctt(1,length(E),length(E))] and then within 
00702    cardinality_totalizer_cl, the two new lists of variables produced would be
00703    [ctt(1,length(E_1).1),...,ctt(1,length(E_1),length(E_1))] 
00704    and 
00705    [ctt(length(E_1)+1,length(E),1)...,ctt(length(E_1)+1,length(E),length(E_2))]. 
00706    </li>
00707   </ul>
00708 
00709 */
00710