Convert constraints to linear form (cpmpy.transformations.linearize)

Transform constraints to a linear form.

This transformation is necessary for Integer Linear Programming (ILP) solvers, and also for translating to Pseudo-Boolean or CNF formats.

There are a number of components to getting a good linearisation: - Decomposing global constraints/functions in a ‘linear friendly’ way.

A common pattern is that constraints that enforce domain consistency on integer variables, that these constraints should be decomposed over a Boolean representation of the domain. This is the case for AllDifferent, Element and possibly others (for now, only done for AllDifferent in this module). Their default decomposition might not do it this way, in which case we want to use different decompositions.

  • Linearising multiplication of variables, e.g. bool*bool, bool*int and int*int. Because ‘*’ is a core Operator and not a global constraint, we need to do it with a helper function here.

  • Disequalities e.g. sum(X) != 5 should be rewritten as (sum(X) < 5) | (sum(X) > 5) and further flattened into implications and linearised.

  • Implications e.g. B -> sum(X) <= 4 should be linearised with the Big-M method.

In principle, but not actually currently implemented: - Domain encodings e.g. of A=cp.intvar(0,4) would create binary variables and constraints

like B0 -> A=0, B1 -> A=1, B2 -> A=2, etc and sum(B0..B4) = 1. However each B0 -> A=0 would require 2 Big-M constraints. Instead we can linearise the entire domain encoding with two constraints: sum(B0..4) = 1 and A = sum(B0..4 * [0,1,2,3,4]). We could even go as far as eliminate the original integer decision variable.

Module functions

Main transformations: - linearize_constraint(): Transforms a list of constraints to a linear form.

Helper functions: - canonical_comparison(): Canonicalizes comparison expressions by moving variables to the

left-hand side and constants to the right-hand side.

Post-linearisation transformations: - only_positive_bv(): Transforms constraints so only boolean variables appear positively

cpmpy.transformations.linearize.canonical_comparison(lst_of_expr: Expression | List[Expression]) → List[Expression][source]

Canonicalize comparison expressions.

Transforms linear expressions, or a reification thereof, into canonical form by: - moving all variables to the left-hand side - moving constants to the right-hand side

Expects the input constraints to be flat. Only apply after applying flatten_constraint().

Parameters:

lst_of_expr – Single expression or list of CPMpy expressions to canonicalize. Can be a single Expression or a list.

Returns:

List of canonicalized CPMpy expressions. All variables are on the left-hand side and all constants are on the right-hand side of comparisons.

cpmpy.transformations.linearize.linearize_constraint(lst_of_expr: List[Expression], supported: Set[str] = {}, csemap: Dict[Expression, _NumVarImpl] | None = None, implication_literal: _BoolVarImpl | NegBoolView | None = None, reified: bool = False) → List[Expression][source]

Transforms all constraints to a linear form. This function assumes all constraints are in ‘flat normal form’ with only boolean variables on the lhs of an implication. Only apply after :func:’cpmpy.transformations.flatten_model.flatten_constraint()’ and :func:’cpmpy.transformations.reification.only_implies()’.

After linearize, the following constraints remain:

Trivial:

  • BoolVal

Linear comparisons:

Equality and non-strict inequality comparison where the left-hand side is a linear expression and the right-hand side is a constant:

  • LinExpr == Constant

  • LinExpr >= Constant

  • LinExpr <= Constant

The linear expression (LinExpr) can be: - A numeric variable (NumVar) - A sum expression (sum([...])) - A weighted sum expression (wsum([weights], [vars]))

General comparisons or expressions, if their name is in `supported`:

  • Boolean expressions: - GenExpr (when is_bool())

  • Numeric comparisons: - GenExpr == Var/Constant (when GenExpr is numeric) - GenExpr <= Var/Constant (when GenExpr is numeric) - GenExpr >= Var/Constant (when GenExpr is numeric)

Indicator constraints, if ‘->’ is in ‘supported’:

The left-hand side is always a Boolean variable or its negation, and the right-hand side can be a linear comparison or a general expression.

  • Linear comparisons: - BoolVar -> LinExpr == Constant - BoolVar -> LinExpr >= Constant - BoolVar -> LinExpr <= Constant

  • General expressions (when the expression name is in supported): - BoolVar -> GenExpr (when GenExpr is boolean) - BoolVar -> GenExpr == Var/Constant (when GenExpr is numeric) - BoolVar -> GenExpr >= Var/Constant (when GenExpr is numeric) - BoolVar -> GenExpr <= Var/Constant (when GenExpr is numeric)

Parameters:

  • lst_of_expr – List of CPMpy expressions to linearize. Must be in ‘flat normal form’ with only boolean variables on the left-hand side of implications.

  • supported – Set of primitive constraint that should not be linearized (e.g. ‘->’, ‘and’, ‘or’, ‘mul’, ‘alldifferent’). ‘->’ in case the solver supports implication constraints ‘and’, ‘or’ in case of e.g. a SAT solver ‘mul’ if the solver supports multiplication of two variables (otherwise it is linearized) ‘alldifferent’ if the solver supports it natively (otherwise this function uses a linear-friendly decomposition)

  • csemap – Optional dictionary for common subexpression elimination, mapping expressions to their flattened variable representations. Used to avoid creating duplicate variables for the same subexpression.

  • implication_literal – when set to, e.g. ‘b’ this means we should linearize b -> lst_of_expr. This is typically done in a recursive call, e.g. this function will call it when encountering a ‘b -> expr’ if ‘->’ is not in supported. When an implication literal is given, a ‘->’ inside it will always be linearized using Big-M even if ‘->’ is in ‘supported’.

  • reified – DEPRECATED, should always be False (use ‘implication_literal’ instead)

Returns:

List of linearized CPMpy expressions. The constraints are in one of the forms described above (linear comparisons, general expressions, or indicator constraints).

cpmpy.transformations.linearize.linearize_mul_comparison(cpm_expr: Comparison, supported: Set[str] = {}, reified: bool = False, csemap: Dict[Expression, _NumVarImpl] | None = None) → Tuple[Expression, List[Expression]][source]

Linearizes multiplication comparisons (const*var | bool*bool | bool*int | int*int) <cmp> rhs.

Parameters:

  • cpm_expr (Comparison) – Comparison to linearize, e.g. bool*bool <cmp> rhs or bool*int <cmp> rhs or int*int <cmp> rhs.

  • supported (Set[str]) – Set of constraint and variable type names that are supported by the target solver, e.g. {“sum”, “wsum”, “->”, “and”, “or”, “alldifferent”}.

  • reified (bool) – Whether the constraint is fully reified. When True, nested implications are linearized using Big-M method instead of indicator constraints.

  • csemap (Optional[Dict[Any, Any]]) – Optional dictionary for common subexpression elimination, mapping expressions to their flattened variable representations. Used to avoid creating duplicate variables for the same subexpression.

Returns:

Tuple of (return expression, list of toplevel constraints) Warning: the return expression is either a linearized comparison, or an ‘and’ of linearized comparisons

cpmpy.transformations.linearize.only_positive_bv(lst_of_expr: List[Expression], csemap: Dict[Any, Any] | None = None) → List[Expression][source]

Replaces Comparison containing NegBoolView with equivalent expression using only BoolVar.

Comparisons are expected to be linearized. Only apply after applying linearize_constraint(cpm_expr). The resulting expression is linear if the original expression was linear.

Parameters:

  • lst_of_expr – List of linearized CPMpy expressions that may contain NegBoolView.

  • csemap – Optional dictionary for common subexpression elimination, mapping expressions to an equivalent decision variable.

Returns:

List of CPMpy expressions where all boolean variables appear positively (no NegBoolView).

cpmpy.transformations.linearize.only_positive_bv_wsum(expr: Expression) → Expression[source]

Replaces a var/sum/wsum expression containing NegBoolView with an equivalent expression using only _BoolVarImpl.

It might add a constant term to the expression, e.g. 3*~b + 2*c is transfromed to 3 + -3*b + 2*c. If you want the constant separately, use only_positive_bv_wsum_const().

Parameters:

expr – Linear expression (NumVar, sum, or wsum) that may contain NegBoolView.

Returns:

Linear expression (NumVar, sum, or wsum) without NegBoolView. The constant term (if any) is incorporated into the expression.

cpmpy.transformations.linearize.only_positive_bv_wsum_const(cpm_expr: Expression) → Tuple[Expression, int][source]

Replaces a var/sum/wsum expression containing NegBoolView with an equivalent expression using only _BoolVarImpl, and returns the constant term separately.

If you want the expression where the constant term is part of the wsum returned, use only_positive_bv_wsum().

Parameters:

cpm_expr – Linear expression (NumVar, sum, or wsum) that may contain NegBoolView.

Returns:

  • pos_expr: Linear expression (NumVar, sum, or wsum) without NegBoolView.

  • const: The constant term that must be added to pos_expr to make it equivalent

    to the original expression.

Return type:

Tuple of

cpmpy.transformations.linearize.only_positive_coefficients(lst_of_expr: List[Expression]) → List[Expression][source]

Replaces Boolean terms with negative coefficients in linear constraints with terms with positive coefficients by negating the literal.

This can simplify a wsum into sum when all coefficients become 1. Input expressions are expected to be canonical comparisons. Only apply after applying canonical_comparison(cpm_expr).

Parameters:

lst_of_expr – List of canonical CPMpy expressions (comparisons) that may contain boolean variables with negative coefficients.

Returns:

List of CPMpy expressions where all boolean variables have positive coefficients. The resulting expression is linear if the original expression was linear.