OKlibrary  0.2.1.6
CardinalityConstraints.hpp File Reference

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 non-negative 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 clause-set generated by cardinality_cl is that, given an arbitrary partial assignment, unit-clause 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 clause-set generated by cardinality_totalizer_cs is that, given an arbitrary partial assignment, unit-clause 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 clause-set generated by cardinality_comparator_cs can be reduced to the empty clause-set (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.