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)

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: dict[Expression, Expression] | 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: dict[Expression, Expression] | 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, min_values=3, csemap=None, ivarmap=None)

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

If ivarmap is None, both sum(bvs)==1 and wsum(values, bvs)==var are posted. If ivarmap is not None, the encoding is added to ivarmap and only sum(bvs)==1 (the domain constraint) is posted; the solver can then choose to eliminate the vars, or post the wsums itself anyway.

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.