Skip to content

Cardinality Constraints

Cardinality constraints CardinalityConstraint are a special type of formulas which enforce that a certain number of variables is assigned to true. They can be of type at least k, exactly k or at most k, for some integer k. Each CardinalityConstraint is a subtype of Formula and offers the same methods as all other formulas. For example, a cardinality constraint of type "at most 1" is:

A + B + C <= 1

And expresses the fact that from the variables A, B, C at most one variable is assigned to true. Meaning the formula is satisfied by exactly 4 assignments

  • A, ~B, ~C
  • ~A, B, ~C
  • ~A, ~B, C
  • ~A, ~B, ~C

At-most-one (AMO) and exactly-one (EXO) constraints play a special role since they are very often used in real world problems. For example if you think of a car configuration, a valid vehicle must have exactly one steering wheel and can have at most one trailer hitch.

Creating Cardinality Constraints

Cardinality constraints can be created using the relevant methods from the formula factory. The methods are:

  • f.cc() for creating a cardinality constraint of any type. The parameters are: Cardinality constraint type, integer for the right-hand side and relevant variables. The possible types are equal EQ, greater than GT, greater than or equal GE, less than LT, or less than or equal LE.
  • f.amo() for creating a cardinality constraints of type "at most one". The parameters are the relevant variables.
  • f.exo() for creating a cardinality constraints of type "exactly one". The parameters are the relevant variables.

The syntax is:

Variable a = f.variable("A");
Variable b = f.variable("B");
Variable c = f.variable("C");

Formula cc = f.cc(CType.GE, 2, Arrays.asList(a, b, c)); // (1)!
Formula amo = f.amo(Arrays.asList(a, b, c)); // (2)!
Formula exo = f.exo(Arrays.asList(a, b, c)); // (3)!
  1. creates cardinality constraint: A + B + C >= 2
  2. creates amo constraint: A + B + C <= 1
  3. creates exo constraint: A + B + C = 1

Of course an AMO constraint can be generated by f.cc(CType.LE, 1, ...) and an EXO constraint by f.cc(CType.EQ, 1, ...) but since they are so common, the formula factory has convenience methods for generating them.

Simplification of Cardinality Constraint on the Formula Factory

Note, that the formula factory methods for amo, exo, and cc return Formula objects and not a CardinalityConstraint. This is due to the fact, that the formula factory simplifies trivial cases like a > 2 to $false or a = 1 to a. Therefore, the result can be a constant or a variable or another formula and does not have to be always a CardinalityConstraint.

Encoding Cardinality Constraints

Some applications, such as SAT solvers, cannot deal with cardinality constraints in their "natural form" (the exception being LogicNG's MiniCard implementation which can handle some type of constraints) since a cardinality constraint is not a purely Boolean construct. Thus, the cardinality constraints have to be encoded to CNF before added to the solver. An encoded cardinality constraint does not contain any signs like <=, >=, <, > and = anymore but is a proper Boolean formula in CNF. There exist many algorithms for encoding cardinality constraints, depending on their type.

LogicNG implements many of these algorithms as described below. If you want to change the encoding of a cardinality constraint using any of these algorithms, you can do this via the cardinality constraint configuration CCConfig, see below. If you don't specify an encoding, then the default encoder is used. The default encoder for a certain cardinality constraint was chosen based on theoretical and practical observations. Most of the encoder algorithms are taken from the MaxSAT solver Open-WBO.

At-most-one Encoder

Encoders of this type encode an at-most-one constraint, so ensure that at most one variable is assigned to true. The implemented algorithms are:

The question which encoding should be used for a specific case heavily depends on the specific use case at hand. It depends on the number of variables in the constraint, the application of the constraint (should it be used on a SAT solver later, in a BDD or a DNNF?), and other considerations like number of newly introduced variables or number of clauses and clause size. The default at-most-one encoder in LogicNG uses the pure encoding without introduction of new variables for up to 10 variables, otherwise it uses the product encoding.

At-most-k and At-least-k Encoder

Encoders of this type encode the generalized version of the AMO constraint: at-most and at-least k constraints. So at most or at least 'rhs' variables can or must be assigned to true. The implemented algorithms are:

Currently, the modular totalizer is the default encoder for at-most-k and at-least-k constraints.

That is, for

Formula amk = f.cc(CType.LE, 2, a, b, c); // A + B + C <= 2
Formula cnf = amk.cnf();

the result is

(~C | x1 | x4) & (~x3 | x1 | x4) & (~x3 | ~C | x4) & (~x4 | x0) & (~x2 | x0) &
(~x4 | ~x2) & (~x4 | ~x2) & (~B | x3 | x5) & (~A | x3 | x5) & (~A | ~B | x5) &
(~x5 | x2) & (~x0 | ~x1)

and for

Formula alk = f.cc(CType.GE, 2, a, b, c); // A + B + C >= 2
Formula cnf = alk.cnf();

(C | x1 | x4) & (~x3 | x1 | x4) & (~x3 | C | x4) & (~x4 | x0) & (~x2 | x0) &
(~x4 | ~x2) & (B | x3 | x5) & (A | x3 | x5) & (A | B | x5) & (~x5 | x2) & (~x0)

Variable Naming

Note that the real formulas' auxiliary variables are named @RESERVED_CC_1 and so on. For the sake of readability we replaced them with x1 in this documentation. The formula factory ensures that the introduced auxiliary variables do not interfere with previously introduced auxiliary variables of other cardinality constraints.

Exactly-k Encoder

Encoders of this type encode the generalized version of the EXO constraint: exactly-k constraints. So exactly 'rhs' variables must be assigned to true. The implemented algorithms are:

Currently, the totalizer encoding is used as default encoder for exactly-k constraints.

Using the Encoder

There are two ways to encode a cardinality constraint

  1. You can encode a constraint manually using the CCEncoder and get a list of clauses of the CNF.
  2. You can call the cnf() method on a cardinality constraint and get the resulting CNF directly.

Consider the cardinality constraint

A + B + C <= 1

You can configure the CCEncoder with a CCConfig object. In this case we explicitly choose the LADDER encoding to generate the CNF for this cardinality constraint. When using the CCEncoder the result ist a list of formulas, each representing a single clause of the encoding's CNF.

CCConfig config =
       CCConfig.builder().amoEncoding(CCConfig.AMO_ENCODER.LADDER).build();
CardinalityConstraint f1 = (CardinalityConstraint) f.amo(Arrays.asList(a, b, c));
List<Formula> encoding = new CCEncoder(f, config).encode(f1);

The result it then the list of clauses (again with replaces auxiliary variables for readability):

[(~A | x1), (~B | x2), (~x1 | x2), (~B | ~x1), (~C | ~x1)]

When calling the cnf() method on the constraint, the default encoding configured in the formula factory is used. So when you change this default for AMO constraint to LADDER beforehand, the result of calling cnf() yield the same result:

CCConfig config =
        CCConfig.builder().amoEncoding(CCConfig.AMO_ENCODER.LADDER).build();
f.putConfiguration(config);
CardinalityConstraint f1 = (CardinalityConstraint) f.amo(Arrays.asList(a, b, c));
Formula encoding = f1.cnf();

The result is the CNF equivalent to the clauses list above:

(~A | x1) & (~B | x2) & (~x1 | x2) & (~B | ~x1) & (~C | ~x1)

Different Cardinality Constraint Encodings

Note that it is not necessary that all cardinality constraints are encoded the same way. It is totally fine to encode different cardinality constraint on the same formula factory with different algorithms.

Incremental Cardinality Constraints

The Cardinality Constraint Encoder in LogicNG has a special mode of operation in combination with a SAT Solver. Often, you do not care for the cardinality constraint encoding in CNF but want to work with the constraint itself. So there is no need to generate the CNF encoding on the formula factory and pollute the factory with all the generated clauses. In this case the encoding can be generated directly on the SAT solver using internal solver variable data structures and never actually generating the formulas on the formula factory. This speeds up computation and saves heap space. Also, there is special version of incremental cardinality constraints where you can tighten the bound of cardinality constraints without generating a new constraint. This is especially useful for optimization problems. We will look at this concept closer in the SAT solving chapter.