How to use the translations of cardinality constraint generators into CNF.
More...
Go to the source code of this file.
Detailed Description
How to use the translations of cardinality constraint generators into CNF.
Cardinality constraints via Maxima in the OKlibrary
Translating cardinality constraints into CNF

Assuming the user has some SAT problem with variable set V, and some subset W of V, for which the user wishes to express that p <= sum(W) <= q, then a clause list representing the additional clauses can be generated in the following way:
W : {1,2,3,4,5}$
p : 2$ q : 4$
F : cardinality_cl([p,listify(W),q]);

New variables of the form ctt(a,b,i) are included in the generated clause list where a and b are integers describing the subset of the variable list which this variable is used to represent the cardinality of (in a unary encoding) and i is a nonnegative integer, (see ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/CardinalityConstraints.mac for further details), and so care must be taken to avoid clashing variables when adding the additional clauses generated by cardinality_cl to the original problem.
Special properties of specific generators

A property of the clauseset generated by cardinality_cl is that, given an arbitrary partial assignment, unitclause propagation will "pick up" any forced assignments.

For example:
F : cl2cs(cardinality_cl([1.[1,2],1]));
ucp_lpa_0_cs(apply_pa_cs({1},F))[2];
[{ctt([],1),ctt([],2)},{2}]
ucp_lpa_0_cs(apply_pa_cs({2},F))[2];
[{ctt([],1),ctt([],2)},{1}]
etc. Notice how, providing the constraint "1 + 2" = 1, and then setting either 1 or 2 to 1, immediately enforces by UCP that variable 2 or 1 (resp.) must be false.

A property of the clauseset generated by cardinality_totalizer_cs is that, given an arbitrary partial assignment, unitclause propagation will immediately pick up any forced assignments. OK: What is the meaning of the next example??? There are NO EXPLANATIONS!

For example:
F : cl2cs(cardinality_totalizer_cl([3,4],[1,2]));
ucp_lpa_0_cs(apply_pa_cs({1},F));
[{{4,2},{2,4}},[{3}]]
ucp_lpa_0_cs(apply_pa_cs({2},F));
[{{4,1},{1,4}},[{3}]]
ucp_lpa_0_cs(apply_pa_cs({4},F));
[{},[{1,2},{3}]]
etc. Notice how, variable 3 is forced by UCP (and is being set to 1) in the cases where 1 or 2 is set to 1, as, in the unary representation 3 must be set to 1 if any variable is set to true.

Given an arbitrary partial assignment, the clauseset generated by cardinality_comparator_cs can be reduced to the empty clauseset (after applying the assignment) by UCP iff no variable in the first m variables of S is set to false, and no variable in the last (length(S)  n) variables is set to true, otherwise it reduces by UCP to the empty clause.
Definition in file CardinalityConstraints.hpp.