From 8b3e1056945f83914958bf754d4a9c4162c1ac7d Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:06:43 +0200 Subject: [PATCH 01/21] implement bv * iv linearization --- cpmpy/transformations/linearize.py | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index d128ba0c7..5d2b62458 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -158,9 +158,25 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, c # linearize unsupported operators elif isinstance(lhs, Operator) and lhs.name not in supported: - if lhs.name == "mul" and is_num(lhs.args[0]): - lhs = Operator("wsum",[[lhs.args[0]], [lhs.args[1]]]) - cpm_expr = eval_comparison(cpm_expr.name, lhs, rhs) + if lhs.name == "mul": + bv_idx = None + if is_num(lhs.args[0]): # const * iv rhs + lhs = Operator("wsum",[[lhs.args[0]], [lhs.args[1]]]) + cpm_expr = eval_comparison(cpm_expr.name, lhs, rhs) + elif isinstance(lhs.args[0], _BoolVarImpl): + bv_idx = 0 + elif isinstance(lhs.args[1], _BoolVarImpl): + bv_idx = 1 + + if bv_idx is not None: + # bv * iv rhs, rewrite to (bv -> iv rhs) & (~bv -> 0 rhs) + bv, iv = lhs.args[bv_idx], lhs.args[1-bv_idx] + bv_true = bv.implies(eval_comparison(cpm_expr.name, iv, rhs)) + bv_false = (~bv).implies(eval_comparison(cpm_expr.name, 0, rhs)) + newlist += linearize_constraint([bv_true, bv_false], supported=supported, reified=reified, csemap=csemap) + continue + else: + raise NotImplementedError(f"Linearization of integer multiplication {cpm_expr} is not supported") elif lhs.name == "pow" and "pow" not in supported: if "mul" not in supported: From 58db38924151ab5d0f1ffe1b11010184d0b652f9 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:12:13 +0200 Subject: [PATCH 02/21] update cplex interface, no support for mul in constraints --- cpmpy/solvers/cplex.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index 79d256ca7..97f1cb336 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -369,7 +369,7 @@ def transform(self, cpm_expr): cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"]), csemap=self._csemap) # supports >, <, != cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) # anything that can create full reif should go above... - cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum", "sub", "min", "max", "abs", "mul"}), csemap=self._csemap) # CPLEX supports quadratic constraints and division by constants + cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum", "sub", "min", "max", "abs"}), csemap=self._csemap) # CPLEX supports quadratic constraints and division by constants cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap) # after linearization, rewrite ~bv into 1-bv return cpm_cons @@ -416,10 +416,6 @@ def add(self, cpm_expr_orig): # a BoundedLinearExpression LHS, special case, like in objective cplexlhs = self._make_numexpr(lhs) self.cplex_model.add_constraint(cplexlhs == cplexrhs) - - elif lhs.name == 'mul': - raise NotImplementedError(f'CPLEX only supports quadratic constraints that define a convex region, i.e. quadratic equalities are not supported: {cpm_expr}') - else: # Global functions if lhs.name == 'min': From 1bd974cbefe9e669b4cfc2c004f3037402f68d51 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:12:37 +0200 Subject: [PATCH 03/21] can keep multiplications in comparisons --- cpmpy/solvers/cplex.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index 97f1cb336..9d3206b6d 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -366,7 +366,7 @@ def transform(self, cpm_expr): cpm_cons = decompose_in_tree(cpm_cons, supported, csemap=self._csemap) cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum', 'sub']), csemap=self._csemap) # constraints that support reification - cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"]), csemap=self._csemap) # supports >, <, != + cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub", "mul"]), csemap=self._csemap) # supports >, <, != cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) # anything that can create full reif should go above... cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum", "sub", "min", "max", "abs"}), csemap=self._csemap) # CPLEX supports quadratic constraints and division by constants From 8499b07786b249800ca49849bd7b1b940f44b69c Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:12:51 +0200 Subject: [PATCH 04/21] add mul in numexpr --- cpmpy/solvers/cplex.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index 9d3206b6d..e54122cf0 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -341,6 +341,10 @@ def _make_numexpr(self, cpm_expr): if cpm_expr.name == "sub": a,b = self.solver_vars(cpm_expr.args) return a - b + + if cpm_expr.name == "mul": + a,b = self.solver_vars(cpm_expr.args) + return a * b raise NotImplementedError("CPLEX: Not a known supported numexpr {}".format(cpm_expr)) From e05df8327acf352fb6653d09baae4f0936e11733 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:13:08 +0200 Subject: [PATCH 05/21] update tests --- tests/test_constraints.py | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index d2d1cada8..fa404cdc9 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -48,9 +48,9 @@ EXCLUDE_OPERATORS = {"gurobi": {}, "pysat": {"mul", "div", "pow", "mod"}, # int2bool but mul, and friends, not linearized "pysdd": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}, - "pindakaas": {"mul", "div", "pow", "mod"}, + "pindakaas": {"mul-int", "div", "pow", "mod"}, "exact": {}, - "cplex": {"mul", "div", "mod", "pow"}, + "cplex": {"mul-int", "div", "mod", "pow"}, "pumpkin": {"pow", "mod"}, } @@ -87,13 +87,15 @@ def numexprs(solver): yield Operator("wsum", [[True, BoolVal(False), np.True_], NUM_ARGS]) # bit of everything continue elif name == "div" or name == "pow": - operator_args = [NN_VAR,3] + yield Operator(name, [NN_VAR,3]) + elif name == "mul" and "mul-int" not in EXCLUDE_OPERATORS.get(solver, {}): + yield Operator(name, NUM_ARGS[:arity]) + elif name == "mul" and "mul-bool" not in EXCLUDE_OPERATORS.get(solver, {}): + yield Operator(name, BOOL_ARGS[:arity]) elif arity != 0: - operator_args = NUM_ARGS[:arity] + yield Operator(name, NUM_ARGS[:arity]) else: - operator_args = NUM_ARGS - - yield Operator(name, operator_args) + yield Operator(name, NUM_ARGS) # boolexprs are also numeric for expr in bool_exprs(solver): From a6386299816d48289b9f73e9691df3add1b75b0f Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:19:09 +0200 Subject: [PATCH 06/21] fix base cas --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 5d2b62458..e4fc1c0dc 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -162,7 +162,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, c bv_idx = None if is_num(lhs.args[0]): # const * iv rhs lhs = Operator("wsum",[[lhs.args[0]], [lhs.args[1]]]) - cpm_expr = eval_comparison(cpm_expr.name, lhs, rhs) + newlist += linearize_constraint([eval_comparison(cpm_expr.name, lhs, rhs)]) elif isinstance(lhs.args[0], _BoolVarImpl): bv_idx = 0 elif isinstance(lhs.args[1], _BoolVarImpl): From 600f70540694cf80c659af377e37f258511758c7 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 15 Oct 2025 12:19:34 +0200 Subject: [PATCH 07/21] pass arguments to recursive call --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index e4fc1c0dc..97d37d86c 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -162,7 +162,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, c bv_idx = None if is_num(lhs.args[0]): # const * iv rhs lhs = Operator("wsum",[[lhs.args[0]], [lhs.args[1]]]) - newlist += linearize_constraint([eval_comparison(cpm_expr.name, lhs, rhs)]) + newlist += linearize_constraint([eval_comparison(cpm_expr.name, lhs, rhs)], supported=supported, reified=reified, csemap=csemap) elif isinstance(lhs.args[0], _BoolVarImpl): bv_idx = 0 elif isinstance(lhs.args[1], _BoolVarImpl): From e672437d5eeff6a010653cfa3a3a115ef2f2d709 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 10:44:11 +0200 Subject: [PATCH 08/21] ensure no BoolVals remain after linearize --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 97d37d86c..f1b0d43a3 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -173,7 +173,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, c bv, iv = lhs.args[bv_idx], lhs.args[1-bv_idx] bv_true = bv.implies(eval_comparison(cpm_expr.name, iv, rhs)) bv_false = (~bv).implies(eval_comparison(cpm_expr.name, 0, rhs)) - newlist += linearize_constraint([bv_true, bv_false], supported=supported, reified=reified, csemap=csemap) + newlist += simplify_boolean(linearize_constraint([bv_true, bv_false], supported=supported, reified=reified, csemap=csemap)) continue else: raise NotImplementedError(f"Linearization of integer multiplication {cpm_expr} is not supported") From c193692b75cc7c55f52ecf1ad3402adcdb6d339b Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 10:44:27 +0200 Subject: [PATCH 09/21] add misisng reified flag --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index f1b0d43a3..7d624977e 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -128,7 +128,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, c continue elif is_false_cst(lin): indicator_constraints=[] # do not add any constraints - newlist+=linearize_constraint([~cond], supported=supported, csemap=csemap) # post linear version of unary constraint + newlist+=linearize_constraint([~cond], supported=supported, csemap=csemap, reified=reified) # post linear version of unary constraint break # do not need to add other else: indicator_constraints.append(cond.implies(lin)) # Add indicator constraint From 12d5cbf2bcdee3873688d4bbda0bdb7cf4769fcf Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 10:44:52 +0200 Subject: [PATCH 10/21] enable tests for pysat --- tests/test_constraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index fa404cdc9..732af2cd6 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -46,7 +46,7 @@ # Exclude certain operators for solvers. # Not all solvers support all operators in CPMpy EXCLUDE_OPERATORS = {"gurobi": {}, - "pysat": {"mul", "div", "pow", "mod"}, # int2bool but mul, and friends, not linearized + "pysat": {"mul-int", "div", "pow", "mod"}, # int2bool but integer-multiplication, and friends, not linearized "pysdd": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}, "pindakaas": {"mul-int", "div", "pow", "mod"}, "exact": {}, From 8e47c8f8a48183a756ccd5ae661c547e121982f2 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 14:20:36 +0200 Subject: [PATCH 11/21] implement big-M for implication constraints --- cpmpy/transformations/linearize.py | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 7d624977e..9623f4c0e 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -70,7 +70,7 @@ from ..expressions.variables import _BoolVarImpl, boolvar, NegBoolView, _NumVarImpl, intvar -def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, csemap=None): +def 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. @@ -130,8 +130,27 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False, c indicator_constraints=[] # do not add any constraints newlist+=linearize_constraint([~cond], supported=supported, csemap=csemap, reified=reified) # post linear version of unary constraint break # do not need to add other - else: + elif "->" in supported and not reified: indicator_constraints.append(cond.implies(lin)) # Add indicator constraint + else: # need to implement using big-M + assert isinstance(lin, Comparison) + assert lin.args[0].name in frozenset({'sum', 'wsum'}), f"Expected sum or wsum as rhs of implication constraint, but got {lin}" + assert is_num(lin.args[1]) + lb, ub = get_bounds(lin.args[0]) + if lin.name == "<=": + M = lin.args[1] - ub # substracting M from lhs will always satisfy the implied constraint + lin.args[0] += M * ~cond + indicator_constraints.append(lin) + elif lin.name == ">=": + M = lin.args[1] - lb # adding M to lhs will always satisfy the implied constraint + lin.args[0] += M * ~cond + indicator_constraints.append(lin) + elif lin.name == "==": + indicator_constraints += linearize_constraint([cond.implies(lin.args[0] <= lin.args[1]), + cond.implies(lin.args[0] >= lin.args[1])], + supported=supported, reified=True, csemap=csemap) + else: + raise ValueError(f"Unexpected linearized rhs of implication {lin} in {cpm_expr}") newlist+=indicator_constraints # ensure no new solutions are created From 43c214926709d5018ccd2547264d6f6191c45d81 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 14:20:47 +0200 Subject: [PATCH 12/21] swap order of transformations --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 9623f4c0e..8937fc594 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -192,7 +192,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal bv, iv = lhs.args[bv_idx], lhs.args[1-bv_idx] bv_true = bv.implies(eval_comparison(cpm_expr.name, iv, rhs)) bv_false = (~bv).implies(eval_comparison(cpm_expr.name, 0, rhs)) - newlist += simplify_boolean(linearize_constraint([bv_true, bv_false], supported=supported, reified=reified, csemap=csemap)) + newlist += linearize_constraint(simplify_boolean([bv_true, bv_false]), supported=supported, reified=reified, csemap=csemap) continue else: raise NotImplementedError(f"Linearization of integer multiplication {cpm_expr} is not supported") From 84d6960c7f2dc8f6a6d4df93d0d3c701b628cc8d Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 14:21:58 +0200 Subject: [PATCH 13/21] update solver interfaces calling linearize --- cpmpy/solvers/cplex.py | 2 +- cpmpy/solvers/exact.py | 2 +- cpmpy/solvers/gurobi.py | 2 +- cpmpy/solvers/pindakaas.py | 2 +- cpmpy/solvers/pysat.py | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index e54122cf0..917bea778 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -373,7 +373,7 @@ def transform(self, cpm_expr): cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub", "mul"]), csemap=self._csemap) # supports >, <, != cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) # anything that can create full reif should go above... - cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum", "sub", "min", "max", "abs"}), csemap=self._csemap) # CPLEX supports quadratic constraints and division by constants + cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum", "->", "sub", "min", "max", "abs"}), csemap=self._csemap) # CPLEX supports quadratic constraints and division by constants cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap) # after linearization, rewrite ~bv into 1-bv return cpm_cons diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 37c00c1b0..553f5181f 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -511,7 +511,7 @@ def transform(self, cpm_expr): cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum"]), csemap=self._csemap) # supports >, <, != cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) # anything that can create full reif should go above... - cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum","mul"}), csemap=self._csemap) # the core of the MIP-linearization + cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum","->","mul"}), csemap=self._csemap) # the core of the MIP-linearization cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap) # after linearisation, rewrite ~bv into 1-bv return cpm_cons diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 9d1e6f012..570b4d95e 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -356,7 +356,7 @@ def transform(self, cpm_expr): cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) # anything that can create full reif should go above... # gurobi does not round towards zero, so no 'div' in supported set: https://github.com/CPMpy/cpmpy/pull/593#issuecomment-2786707188 - cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","sub","min","max","mul","abs","pow"}), csemap=self._csemap) # the core of the MIP-linearization + cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","->","sub","min","max","mul","abs","pow"}), csemap=self._csemap) # the core of the MIP-linearization cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap) # after linearization, rewrite ~bv into 1-bv return cpm_cons diff --git a/cpmpy/solvers/pindakaas.py b/cpmpy/solvers/pindakaas.py index 20540903a..66cefc3d0 100755 --- a/cpmpy/solvers/pindakaas.py +++ b/cpmpy/solvers/pindakaas.py @@ -238,7 +238,7 @@ def transform(self, cpm_expr): cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) cpm_cons = linearize_constraint( - cpm_cons, supported=frozenset({"sum", "wsum", "and", "or"}), csemap=self._csemap + cpm_cons, supported=frozenset({"sum", "wsum", "->", "and", "or"}), csemap=self._csemap ) cpm_cons = int2bool(cpm_cons, self.ivarmap, encoding=self.encoding) return cpm_cons diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index def9e6804..1525058d1 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -371,7 +371,7 @@ def transform(self, cpm_expr): cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form cpm_cons = only_bv_reifies(cpm_cons, csemap=self._csemap) cpm_cons = only_implies(cpm_cons, csemap=self._csemap) - cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum", "and", "or"}), csemap=self._csemap) # the core of the MIP-linearization + cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum", "->", "and", "or"}), csemap=self._csemap) # the core of the MIP-linearization cpm_cons = int2bool(cpm_cons, self.ivarmap, encoding=self.encoding) cpm_cons = only_positive_coefficients(cpm_cons) return cpm_cons From 7d637880dc90961310df35d1005acb5ee8c2287d Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 15:09:06 +0200 Subject: [PATCH 14/21] update comment --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 8937fc594..1e8daa6ed 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -138,7 +138,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal assert is_num(lin.args[1]) lb, ub = get_bounds(lin.args[0]) if lin.name == "<=": - M = lin.args[1] - ub # substracting M from lhs will always satisfy the implied constraint + M = lin.args[1] - ub # subtracting M from lhs will always satisfy the implied constraint lin.args[0] += M * ~cond indicator_constraints.append(lin) elif lin.name == ">=": From c61cb85ca7c39bfed8afa6bbc1d3fb55e765141a Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 15:09:18 +0200 Subject: [PATCH 15/21] condition of impl is not new var --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 1e8daa6ed..0bad19e4b 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -154,7 +154,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal newlist+=indicator_constraints # ensure no new solutions are created - new_vars = set(get_variables(lin_sub)) - set(get_variables(sub_expr)) + new_vars = set(get_variables(lin_sub)) - set(get_variables(sub_expr)) - {cond, ~cond} newlist += linearize_constraint([(~cond).implies(nv == nv.lb) for nv in new_vars], supported=supported, reified=reified, csemap=csemap) else: # supported operator From 26876c37f691988f15252fb66a3430e09f699771 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 15:09:23 +0200 Subject: [PATCH 16/21] add tests --- tests/test_trans_linearize.py | 67 +++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) diff --git a/tests/test_trans_linearize.py b/tests/test_trans_linearize.py index 87c0c0178..ba42cae70 100644 --- a/tests/test_trans_linearize.py +++ b/tests/test_trans_linearize.py @@ -238,6 +238,73 @@ def test_sub(self): [lin_cons] = linearize_constraint([cons]) self.assertEqual(str(lin_cons), "sum([1, -1] * [x, y]) == 3") + def test_bool_mult(self): + + x = cp.intvar(-5, 10, name="x") + y = cp.intvar(-5, 10, name="y") + a = cp.boolvar(name="a") + b = cp.boolvar(name="b") + + def assert_cons_is_true(cons): + return lambda : self.assertTrue(cons.value()) + + cons = b * x == y + bt,bf = linearize_constraint([cons]) + self.assertEqual(str(bt), "(b) -> (sum([1, -1] * [x, y]) == 0)") + self.assertEqual(str(bf), "(~b) -> (sum([y]) == 0)") + + cp.Model([bt,bf]).solveAll(display=assert_cons_is_true(cons)) + + cons = x * b == y + bt,bf = linearize_constraint([cons]) + self.assertEqual(str(bt), "(b) -> (sum([1, -1] * [x, y]) == 0)") + self.assertEqual(str(bf), "(~b) -> (sum([y]) == 0)") + + cp.Model([bt,bf]).solveAll(display=assert_cons_is_true(cons)) + + cons = a.implies(b * x <= y) + lin_cons = linearize_constraint([cons]) + self.assertEqual(str(lin_cons[0]), "(a) -> (sum([1, -1, -15] * [x, y, ~b]) <= 0)") + self.assertEqual(str(lin_cons[1]), "(a) -> (sum([1, 5] * [y, b]) >= 0)") + + lin_cnt = cp.Model(lin_cons).solveAll(display=assert_cons_is_true(cons)) + cons_cnt = cp.Model(cons).solveAll(display=assert_cons_is_true(cp.all(lin_cons))) + self.assertEqual(lin_cnt, cons_cnt) + + cons = a.implies(b * x >= y) + lin_cons = linearize_constraint([cons]) + self.assertEqual(str(lin_cons[0]), "(a) -> (sum([1, -1, 15] * [x, y, ~b]) >= 0)") + self.assertEqual(str(lin_cons[1]), "(a) -> (sum([1, -10] * [y, b]) <= 0)") + + lin_cnt = cp.Model(lin_cons).solveAll(display=assert_cons_is_true(cons)) + cons_cnt = cp.Model(cons).solveAll(display=assert_cons_is_true(cp.all(lin_cons))) + self.assertEqual(lin_cnt, cons_cnt) + + + def test_implies(self): + + x = cp.intvar(1, 10, name="x") + y = cp.intvar(1, 10, name="y") + b = cp.boolvar(name="b") + + cons = b.implies(x + y <= 5) + [lin_cons] = linearize_constraint([cons], supported={"sum", "wsum"}) # no support for "->" + self.assertEqual(str(lin_cons), "sum([1, 1, -15] * [x, y, ~b]) <= 5") + + cons = b.implies(x + y >= 5) + [lin_cons] = linearize_constraint([cons], supported={"sum", "wsum"}) # no support for "->" + self.assertEqual(str(lin_cons), "sum([1, 1, 3] * [x, y, ~b]) >= 5") + + cons = b.implies(x + y == 5) + lin_cons = linearize_constraint([cons], supported={"sum", "wsum"}) # no support for "->" + assert len(lin_cons) == 2 + self.assertEqual(str(lin_cons[0]), "sum([1, 1, -15] * [x, y, ~b]) <= 5") + self.assertEqual(str(lin_cons[1]), "sum([1, 1, 3] * [x, y, ~b]) >= 5") + + + + + class TestConstRhs(unittest.TestCase): From b139681bf24b75f342f2a0ef081f54931907e7d4 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 15:59:44 +0200 Subject: [PATCH 17/21] unlikely case where reified global func is supported --- cpmpy/transformations/linearize.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 0bad19e4b..3746bdc5e 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -132,8 +132,14 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal break # do not need to add other elif "->" in supported and not reified: indicator_constraints.append(cond.implies(lin)) # Add indicator constraint - else: # need to implement using big-M + else: # Nested -> or implication constraints are not supported assert isinstance(lin, Comparison) + if lin.args[0].name not in {"sum", "wsum"}: + assert lin.args[0].name in supported, f"Unexpected rhs of implication: {lin}, it is not supported ({supported})" + indicator_constraints.append(cond.implies(lin)) + continue + + # need to write as big-M assert lin.args[0].name in frozenset({'sum', 'wsum'}), f"Expected sum or wsum as rhs of implication constraint, but got {lin}" assert is_num(lin.args[1]) lb, ub = get_bounds(lin.args[0]) From 085920b2cca913ca54d226861ab8115f9fd01f58 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 20 Oct 2025 15:59:55 +0200 Subject: [PATCH 18/21] mssing continue --- cpmpy/transformations/linearize.py | 1 + 1 file changed, 1 insertion(+) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index 3746bdc5e..e2dd094a8 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -188,6 +188,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal if is_num(lhs.args[0]): # const * iv rhs lhs = Operator("wsum",[[lhs.args[0]], [lhs.args[1]]]) newlist += linearize_constraint([eval_comparison(cpm_expr.name, lhs, rhs)], supported=supported, reified=reified, csemap=csemap) + continue elif isinstance(lhs.args[0], _BoolVarImpl): bv_idx = 0 elif isinstance(lhs.args[1], _BoolVarImpl): From f293c14093fa68318a440b124270c7c15d62378f Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 16:57:24 +0200 Subject: [PATCH 19/21] reified is not always true --- cpmpy/transformations/linearize.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index e2dd094a8..fb8d8673f 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -154,7 +154,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal elif lin.name == "==": indicator_constraints += linearize_constraint([cond.implies(lin.args[0] <= lin.args[1]), cond.implies(lin.args[0] >= lin.args[1])], - supported=supported, reified=True, csemap=csemap) + supported=supported, reified=reified, csemap=csemap) else: raise ValueError(f"Unexpected linearized rhs of implication {lin} in {cpm_expr}") newlist+=indicator_constraints From 5719c8b906da1bf7e7720b966ce6043d5c9d1422 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 8 Dec 2025 13:00:13 +0100 Subject: [PATCH 20/21] update comment --- cpmpy/transformations/linearize.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py index fb8d8673f..b8ca87efe 100644 --- a/cpmpy/transformations/linearize.py +++ b/cpmpy/transformations/linearize.py @@ -128,12 +128,13 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum","->"}, reified=Fal continue elif is_false_cst(lin): indicator_constraints=[] # do not add any constraints - newlist+=linearize_constraint([~cond], supported=supported, csemap=csemap, reified=reified) # post linear version of unary constraint + newlist += linearize_constraint([~cond], supported=supported, csemap=csemap, reified=reified) # post linear version of unary constraint break # do not need to add other elif "->" in supported and not reified: indicator_constraints.append(cond.implies(lin)) # Add indicator constraint - else: # Nested -> or implication constraints are not supported - assert isinstance(lin, Comparison) + else: # need to linearize the implication constraint itself + # either -> is not supported, or we are in a reified context (nested -> constraints are not linear) + assert isinstance(lin, Comparison), f"Expected a comparison as rhs of implication constraint, got {lin}" if lin.args[0].name not in {"sum", "wsum"}: assert lin.args[0].name in supported, f"Unexpected rhs of implication: {lin}, it is not supported ({supported})" indicator_constraints.append(cond.implies(lin)) From b647b3717cd85d63fcc660ae831fecffa0015e0e Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Mon, 8 Dec 2025 14:57:51 +0100 Subject: [PATCH 21/21] update test_constraints --- tests/test_constraints.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 856510e20..a41ab5fde 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -86,15 +86,15 @@ def numexprs(solver): yield Operator("wsum", [list(range(len(NUM_ARGS))), NUM_ARGS]) yield Operator("wsum", [[True, BoolVal(False), np.True_], NUM_ARGS]) # bit of everything continue - elif name == "mul": - yield Operator(name, [3,NUM_ARGS[0]]) - yield Operator(name, NUM_ARGS[:2]) - if solver != "minizinc": # bug in minizinc, see https://github.com/MiniZinc/libminizinc/issues/962 - yield Operator(name, [3,BOOL_ARGS[0]]) elif name == "div" or name == "pow": yield Operator(name, [NN_VAR,3]) elif name == "mul" and "mul-int" not in EXCLUDE_OPERATORS.get(solver, {}): + yield Operator(name, [3, NUM_ARGS[0]]) yield Operator(name, NUM_ARGS[:arity]) + yield Operator(name, NUM_ARGS[:2]) + if solver != "minizinc": # bug in minizinc, see https://github.com/MiniZinc/libminizinc/issues/962 + yield Operator(name, [3, BOOL_ARGS[0]]) + elif name == "mul" and "mul-bool" not in EXCLUDE_OPERATORS.get(solver, {}): yield Operator(name, BOOL_ARGS[:arity]) elif arity != 0: