OKlibrary
0.2.1.6

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 nonroot 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((ba+1)/2)], 00350 [[a,b], 00351 unary_addition_tree_1r_lrt(a,a+d1), 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 inputliteral i, while inner nodes have labels [a,b], 00359 corresponding to auxiliary variables vru(a,b,1), ..., vru(a,b,ba+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 : ba+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+d1), 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 clauseset describing the relation 00376 between a nonleaf %node and its two children is needed, and then the 00377 totaliserfunction 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 clauselist 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 unitclausepropagation 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 clauseset. 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 clauselists 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 unitclauses 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)/21),1),..., 00509 vru(a,ceiling((a+b)/21),floor(length(E)/2))], 00510 a,floor((a+b)/2)), 00511 vc([vru(ceiling((a+b)/21)+1,b,1),..., 00512 vru(ceiling((a+b)/21)+1,ceiling(length(E)/2))], 00513 ceiling((a+b)/21)+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 ba = 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 ba = 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 ba > 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/21),j)) and phi(vru(ceiling(a+b/21)+1,b,k)) 00555 00556 i.e., in each case [vru(a,b,1),...,vru(a,b,ba+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,bb')] respectively depending on 00560 a and b, where b' = ceiling((a+b)/21). 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 addercircuit 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 "Pseudoboolean 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 PseudoBoolean 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 pseudoboolean 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 clausesets(!)). </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