OKlibrary
0.2.1.6

Plans for translations of cardinality constraints into CNF. More...
Go to the source code of this file.
Plans for translations of cardinality constraints into CNF.
C : ["cardinality", "<", {v1,v2,v3}, 6]; Cs : subst(C[2], r, r(sum_l(listify(C[3])), C[4])); v3v2+v1 < 6 Csa : at(Cs, [v1=1, v2=0, v3=1]); 2 < 6 is(Csa); true
unary_addition_tree_0_lrt(n) := if n=1 then [[1]] else block([a : floor(n/2), b], b : n  a, return([[n], unary_addition_tree_0_lrt(a), unary_addition_tree_0_lrt(b)]))$ draw_lrt_dbl(unary_addition_tree_0_lrt(5),d:inf); /* Should be draw_lrt(unary_addition_tree_0_lrt(5),d:inf); */
unary_addition_tree_1_lrt(n) := unary_addition_tree_1r_lrt(1,n)$ /* Prerequisite: a, b natural numbers, a <= b */ unary_addition_tree_1r_lrt(a,b) := if a=b then [a] else block([d : floor((ba+1)/2)], [[a,b], unary_addition_tree_1r_lrt(a,a+d1), unary_addition_tree_1r_lrt(a+d,b)])$ draw_lrt_dbl(unary_addition_tree_1_lrt(5)); /* draw_lrt(unary_addition_tree_1_lrt(5),d:inf); */
unary_addition_tree_2_lrt(L) := unary_addition_tree_2r_lrt(L,1,length(L))$ unary_addition_tree_2r_lrt(L,a,b) := block([l : ba+1], if l = 1 then L else block([d : floor(l/2)], [create_list(vru_var(a,b,i),i,1,l), unary_addition_tree_2r_lrt(take_elements(d,L),a,a+d1), unary_addition_tree_2r_lrt(rest(L,d),a+d,b)]))$ draw_lrt_dbl(unary_addition_tree_2_lrt([a,b,c,d,e])); /* draw_lrt(unary_addition_tree_2_lrt(5),d:inf); */
unary_bb_add_fcl(A,B,C) := block([F:[]], for alpha : 0 thru length(A) do for beta : 0 thru length(B) do block([sigma : alpha+beta], if sigma > 0 then F : cons(union( if alpha > 0 then {A[alpha]} else {}, if beta > 0 then {B[beta]} else {}, {C[sigma]}), F), if sigma < length(C) then F : cons(union( if alpha < length(A) then {A[alpha+1]} else {}, if beta < length(B) then {B[beta+1]} else {}, {C[sigma+1]}),F) ), return([stable_unique(map(var_l,append(A,B,C))),F]))$
A CNF representation of a boolean cardinality constraint [a,L,b] with "detection of forced assignments via UCP" is a CNF representation of [a,L,b] with the property that for every partial assignment phi with var(phi) <= var(L) and every forced assignment <v > e> for apply_pa(phi,F) with v in var(L), applying unitclausepropagation to apply_pa(phi,F) includes this forced assignment (i.e., UCP derives all forced assignments for apply_pa(phi,F) which concern the cardinality constraint).
The following algorithm, from the above mentioned paper, computes a CNF representation F of the cardinality constraint [a,L,b] with detection of forced assignments via UCP. The algorithm takes as input a list E of literals, and then introduces a list of new (distinct) variables S of the same size as E, which under any assignment will have the unary representation (ones/trues appearing from the left) of the cardinality of E. The remainder of the algorithm consists of two phases, the totalizer and the comparator, and the clauses generated (and variables introduced) by these phases are then appended together to produce the final clauseset. The totalizer enforces that S is the unary representation of the cardinality of L and the comparator enforces that this unary representation represents a number in the range a to b. The totalizer takes as input a list E of input variables, and as output a list S of cardinality variables, and returns a list of clauses that enforce that S is a unary representation of E. This is done in a recursive manner, through the introduction of new variables, and clauses enforcing unary addition. In the totalizer, E is split into two sublists E_1 and E_2, where E_1 is the list of the first floor(length(E)/2) elements and E_2 is the remainder of E. The algorithm then introduces two lists of new (distinct) variables S_1 and S_2, where S_1 and S_2 are the same size as E_1 and E_2 respectively. Totalizer is then run again for each of these sublists E_1 with S_1 and E_2 with S_2 returning (new) variable and clauselists V_1,C_1 and V_2,C_2 respectively, and then the following clauses (C_3) are generated to enforce that in any satisfying assignment of F, we have that S is the unary addition of S_1 and S_2: for every 0 <= a <= length(E_1) and 0 <= b <= length(E_2) and 0 <= c <= length(L) such that a + b = c we add the clauses 1) {S_1[a],S_2[b],S[c]} and 2) {S_1[a+1], S_2[b+1], S[c+1]} where (1) ensures (S_1[a] and S_2[b]) => S[a+b]), i.e., the unary addition holds in one direction and (2) ensures (S[a+b+1] => (S_1[a+1] or S_2[b+1]), i.e., the other direction, and we have S_1[0] = S_2[0] = S[0] = 1 and S_1[length(E_1)+1] = S_2[length(E_2)+1] = S[length(L)+1] = 0 for the extreme cases for the above clauses. In the base case where length(E) = 1, totalizer takes S_1 = E_1, and S_2 = E2, since E_1 and E_2 are their own unary representations. The comparator generates a list of unitclauses [{S[1]},...,{S[a]},{S[b+1]},...,{S[length(L)]}] which ensures that, given that the totalizer ensures that S is the unary representation of the cardinality of E, any satisfying assignment which results in E having a cardinality less than a, or greater than b, is a falsifying assignment for F. To use this algorithm see unary_bb_crd2fcl.
The list of new variables introduced by this function can therefore be recursively defined using a function vc, where V = rest(vc(E,1,length(E)), length(E)): vc(E,a,b) = [] if a == b else append( E, vc([vru(a,ceiling((a+b)/21),1),..., vru(a,ceiling((a+b)/21),floor(length(E)/2))], a,floor((a+b)/2)), vc([vru(ceiling((a+b)/21)+1,b,1),..., vru(ceiling((a+b)/21)+1,ceiling(length(E)/2))], ceiling((a+b)/21)+1,b)) Therefore the number of new variables introduced given length(E) = n is nvc(n)  n where nvc is defined recursively in the following way: nvc(n) = 0 if n < 1 n + nvc(floor(n/2)) + nvc(ceiling(n/2)) otherwise Assuming S is without complimentary literals, a partial assignment phi satisfies F iff phi is total and given n is the cardinality of E under phi, we have that phi(S[i]) = 1 for 1 <= i <= n and phi(S[i]) = 0 for i > n, and given m is the cardinality of E[1,...,floor(length(E)/2)] we have phi(vru(1,floor(length(E)/2),i)) = 1 for 1 <= i <= m and phi(vru(1,floor(length(E)/2),i)) = 0 otherwise and given m' is the cardinality of E[floor(length(E)/2)+1,...,length(E)] we have phi(vru(floor(length(E)/2)+1,length(E),i)) = 1 for 1 <= i <= m' and phi(vru(floor(length(E)/2)+1,length(E),i)) = 0 otherwise and for all a and b such that we have a new variable vru(a,b,i) for some i, if ba = 2 then we have phi(vru(a,b,1)) = phi(E[a]) xor phi(E[b]) phi(vru(a,b,2)) = phi(E[a]) and phi(E[b]) if ba = 3 then we have phi(vru(a,b,1)) = phi(E[a]) or phi(vru(a+1,b,1)) phi(vru(a,b,2)) = (phi(E[a]) and phi(vru(a+1,b,1))) or phi(vru(a+1,b,2)) phi(vru(a,b,3)) = phi(E[a]) and phi(vru(a+1,b,2)) and if ba > 3 then we have phi(vru(a,b,i)) = there exist j,k such that j+k=i phi(vru(a,ceiling(a+b/21),j)) and phi(vru(ceiling(a+b/21)+1,b,k)) i.e., in each case [vru(a,b,1),...,vru(a,b,ba+1)] is the representation of the unary addition of E[a] and E[b], E[a] and [vru(a+1,b,1),vru(a+1,b,2)] or [vru(a,b',1),...,vru(a,b',b'a+1)] and [vru(b'+1,b,1),...,vru(b'+1,b,bb')] respectively depending on a and b, where b' = ceiling((a+b)/21). unary_bb_totalizer_r_fcl is a function with additional parameters to keep track of any new variables introduced, and has the same specification as unary_bb_totaliser_fcl, except V = rest(vc(E,a,b), length(E)).
Definition in file CardinalityConstraints.hpp.