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
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:
And expresses the fact that from the variables
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
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:
- creates cardinality constraint: A + B + C >= 2
- creates amo constraint: A + B + C <= 1
- 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
Formula objects and not a
CardinalityConstraint. This is due to the fact, that the formula factory simplifies trivial cases like
a > 2 to
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
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
= 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.
Encoders of this type encode an at-most-one constraint, so ensure that at most one variable is assigned to
The implemented algorithms are:
- Pure: This algorithm uses the 'naive' encoding with no introduction of new variables but quadratic size. I.e. introducing pair-wise constraints that each variable set to true forces all other variables to false. E.g. the constraint
A + B + C <= 1is translated to
(A => ~B) & (A => ~C) & (B => ~A) & (B => ~C) & (C => ~A) & (C => ~B)simplified to the CNF
(~A | ~B) & (~A | ~C) & (~B | ~C)
- Ladder: This algorithm uses the Ladder/Regular Encoding due to Gent & Nightingale.
- Product: This algorithm uses the 2-Product Method due to Chen.
- Nested: This algorithm uses the nested encoding.
- Commander: This algorithm uses the Commander Encoding due to Klieber & Kwon
- Binary: This algorithm uses the Binary Encoding due to Doggett, Frisch, Peugniez, and Nightingale.
- Bimander. Uses the Bimander Encoding due to Hölldobler and Nguyen. When choosing this algorithm, one can also describe the group size: Half, square-root, fixed.
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:
- Cardinality Network for at most k, Cardinality Network for at least k: This algorithm uses the Cardinality Network Encoding due to Asín, Nieuwenhuis, Oliveras, and Rodríguez-Carbonell
- Totalizer for at most k, Totalizer for at least k: This algorithm uses the Totalizer Encoding due to Bailleux and Boufkhad
- Modulo Totalizer for at most k, Modulo Totalizer for at least k: This algorithm uses the Module Totalizer due to Ogawa, Liu, Hasegawa, Koshimura & Fujita
Currently, the modular totalizer is the default encoder for at-most-k and at-least-k constraints.
That is, for
the result is
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.
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:
- Totalizer: Uses the Totalizer Encoding due to Bailleux and Boufkhad for translating the cardinality constraint into CNF
- Cardinality Network: Uses the cardinality network encoding due to Cardinality Network Encoding due to Asín, Nieuwenhuis, Oliveras, and Rodríguez-Carbonell
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
- You can encode a constraint manually using the CCEncoder and get a list of clauses of the CNF.
- You can call the
cnf()method on a cardinality constraint and get the resulting CNF directly.
Consider the cardinality constraint
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.
The result it then the list of clauses (again with replaces auxiliary variables for readability):
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:
The result is the CNF equivalent to the clauses list above:
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.