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 SAT solvers.

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 other functions listed in get_linear_decompositions(). Their default decomposition does not do it this way, hence we use a more linear-friendly decomposition. This is done by decompose_linear().

• Domain encodings constraint (x == 3) + (x == 5) + (x == 7) >= 1 after flattening will introduce Boolean auxiliary variables and constraints Bx3 == (x == 3), Bx5 == (x == 5), Bx7 == (x == 7) and sum(Bx3, Bx5, Bx7) >= 1. However each Bxi == (x == i) would be linearized into 3 Big-M constraints. Instead we can linearise the entire domain encoding of x for all i values in its domain with just two constraints: sum_i(Bxi) = 1 and x = sum_i(i*Bxi). This is done by linearize_reified_variables() (as a pre-linearization optimization step).

• Disequalities and Inequalities e.g. sum(X) != 5 should be rewritten as (sum(X) < 5) | (sum(X) > 5), which is then further flattened into implications. Strict equalities like sum(X) > 5 are in turn rewritten to non-strict inequalities, e.g. sum(X) >= 6. This is done by linearize_constraint().

• Implications and Big-M e.g. B -> sum(X) <= 4 should be linearised with the Big-M method, if not natively supported. This is done by linearize_constraint(). If it is natively supported, then the supported argument should contain ‘->’.

To get a good linearisation, solver backends typically apply these transformations in roughly this order:

• Call decompose_linear() / decompose_linear_objective() instead of the standard ‘decompose_in_tree’.

• Put constraints in flat normal form (flatten_constraint()).

• Apply linearize_reified_variables() to replace reified equalities of the form bv == (x == val) by a single direct encoding of x (must be done before implication-only normalisation).

• Ensure implications are of the form bv -> <expr> (only_implies()).

• Call linearize_constraint() to transform the inequalities, strict equalities and implications.

• Optionally run post-passes such as only_positive_bv() (e.g. for ILP solvers that do not support NegBoolView) and only_positive_coefficients() (e.g. for PB solvers that want it in this normal form)

Module functions

Main transformations: - linearize_constraint(): Transforms a list of constraints to a linear form. - decompose_linear(): Decompose unsupported global constraints in a linear-friendly way. - decompose_linear_objective(): Decompose objective using linear-friendly decompositions. - linearize_reified_variables(): For an integer x with (BV == (x == val)) constraints, replace them with the direct encoding of ‘x’.

Helper functions: - canonical_comparison(): Canonicalize comparison expressions (variables on left, constants on right). - get_linear_decompositions(): Returns the custom linear decomposition map for global constraints.

Optional post-linearisation transformations: - only_positive_bv(): Transforms constraints so only _BoolVarImpl variables appear positively

(no NegBoolView).

• only_positive_bv_wsum(): Helper function that replaces NegBoolView in var/sum/wsum expressions with equivalent expressions using only _BoolVarImpl.

• only_positive_bv_wsum_const(): Same as only_positive_bv_wsum() but returns the constant term separately.

• only_positive_coefficients(): Transforms constraints so only positive coefficients appear in linear constraints.

cpmpy.transformations.linearize.canonical_comparison(lst_of_expr: Sequence[Expression] | ndarray) → list[Expression]

Canonicalize a comparison expression. 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()

cpmpy.transformations.linearize.decompose_linear(lst_of_expr: Sequence[Expression], supported: AbstractSet[str] | None = None, supported_reified: AbstractSet[str] | None = None, csemap: CSEMap | None = None)

Decompose unsupported global constraints in a linear-friendly way using (var == val) in sums.

Parameters:

• lst_of_expr – list of expressions to decompose

• supported – set of supported global constraints and global functions

• supported_reified – set of supported reified global constraints

• csemap – map of expressions to an auxiliary variable

Returns:

list of expressions

cpmpy.transformations.linearize.decompose_linear_objective(obj: Expression, supported: AbstractSet[str] | None = None, supported_reified: AbstractSet[str] | None = None, csemap: CSEMap | None = None)

Decompose objective using linear-friendly (var == val) decompositions.

cpmpy.transformations.linearize.get_linear_decompositions()

Implementation of custom linear decompositions for some global constraints. Uses (var == val) in sums; no integer encoding.

Returns:

a dictionary mapping expression names to a function, taking as argument the expression to decompose

Return type:

dict

cpmpy.transformations.linearize.linearize_constraint(lst_of_expr, supported={'->', 'sum', 'wsum'}, reified=False, csemap=None)

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()’.

Parameters:

• supported – which constraint and variable types are supported, i.e. sum, and, or, alldifferent AllDifferent has a special linearization and is decomposed as such if not in supported. Any other unsupported global constraint should be decomposed using cpmpy.transformations.decompose_global.decompose_in_tree()

• reified – whether the constraint is fully reified

cpmpy.transformations.linearize.linearize_reified_variables(constraints: list[Expression], min_values: int = 3, csemap: CSEMap | None = None, ivarmap: dict[str, IntVarEnc] | None = None) → list[Expression]

Replace reified (BV <-> (x == val)) implications with direct encoding and reified (BV <-> (x >= val)) implications with order encoding when a variable has at least min_values such reifications: remove those implications and add the corresponding encoding of x.

If ivarmap is None, both consistency constraints and channeling constraints are posted. If ivarmap is not None, the encoding is added to ivarmap and only (the domain constraint) is posted; the solver can then choose to eliminate the variables, or post the channeling constraints itself anyway.

If both BV <-> (x == val) and BV <-> (x >= val) are present, choose the encoding type that occurs most often for that variable. Ties prefer the direct encoding. (TODO: add both encodings and channel between them?)

Apply AFTER flatten_constraint and BEFORE only_implies and linearize_constraint.

cpmpy.transformations.linearize.only_positive_bv(lst_of_expr, csemap=None)

Replaces Comparison containing NegBoolView with equivalent expression using only BoolVar. Comparisons are expected to be linearized. Only apply after applying linearize_constraint(cpm_expr).

Resulting expression is linear if the original expression was linear.

cpmpy.transformations.linearize.only_positive_bv_wsum(expr)

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

It might add a constant term to the expression, if you want the constant separately, use only_positive_bv_wsum_const().

Arguments: - cpm_expr: linear expression (sum, wsum, var)

Returns tuple of: - pos_expr: linear expression (sum, wsum, var) without NegBoolView

cpmpy.transformations.linearize.only_positive_bv_wsum_const(cpm_expr)

Replaces a var/sum/wsum expression containing NegBoolView with an equivalent expression using only BoolVar as well as a constant term that must be added to the new expression to be equivalent.

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

Arguments: - cpm_expr: linear expression (sum, wsum, var)

Returns tuple of: - pos_expr: linear expression (sum, wsum, var) without NegBoolView - const: The difference between the original expression and the new expression,

i.e. a constant term that must be added to pos_expr to be an equivalent linear expression.

cpmpy.transformations.linearize.only_positive_coefficients(lst_of_expr)

Replaces Boolean terms with negative coefficients in linear constraints with terms with positive coefficients (including 0) by negating its literal. This can simplify a wsum into sum. cpm_expr is expected to be a canonical comparison. Only apply after applying canonical_comparison(cpm_expr)

Resulting expression is linear.

cpmpy.transformations.linearize.only_positive_coefficients_(ws, xs)

Helper function to replace Boolean terms with negative coefficients with terms with positive coefficients (including 0) in Boolean linear expressions, given as a list of coefficients ws and a list of Boolean variables xs. Returns new non-negative coefficients and variables, and a constant term to be added.