Repository: CPMpy/cpmpy

Issue:
var comp sum optimisation
bv0 > bv2 + bv3
creates an intvar for the lhs instead of normalising as:
bv0 - (bv2 + bv3) > 0

This is a blocker for #114 which should stay in pseudo-boolean space.

should probably be handled somewhere in flatten's normalize_boolexpr (because the '>' comparison is bool); not sure.

```
import cpmpy as cp
bvs = cp.boolvar(3)
c = bvs[0] > sum(bvs[1:])
s = cp.SolverLookup.get("pysat")
print(c, "==>", s.transform(c))
s += c
s.solve()
```

Discussion:

Solution patch:
diff --git a/.github/workflows/python-test.yml b/.github/workflows/python-test.yml
index 6e20450f..173322ba 100644
--- a/.github/workflows/python-test.yml
+++ b/.github/workflows/python-test.yml
@@ -16,7 +16,7 @@ jobs:
       - name: Install dependencies
         run: |
           python -m pip install --upgrade pip
-          pip install flake8 pytest requests pandas
+          pip install flake8 pytest pytest-xdist requests pandas
           if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
           pip install python-sat
           pip install z3-solver
@@ -27,5 +27,5 @@ jobs:
           pip install minizinc
       - name: Test with pytest
         run: |
-          python -m pytest tests/
+          python -m pytest -n 4 tests/
 
diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py
index 60a98493..33647f2e 100644
--- a/cpmpy/expressions/core.py
+++ b/cpmpy/expressions/core.py
@@ -433,6 +433,9 @@ class BoolVal(Expression):
         """Called to implement truth value testing and the built-in operation bool(), return stored value"""
         return self.args[0]
 
+    def get_bounds(self):
+        v = int(self.args[0])
+        return (v,v)
 
     def has_subexpr(self) -> bool:
         """ Does it contains nested Expressions (anything other than a _NumVarImpl or a constant)?
diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py
index b3d0c782..602f2e8b 100644
--- a/cpmpy/solvers/pysat.py
+++ b/cpmpy/solvers/pysat.py
@@ -39,9 +39,10 @@
 """
 from .solver_interface import SolverInterface, SolverStatus, ExitStatus
 from ..exceptions import NotSupportedError
-from ..expressions.core import Expression, Comparison, Operator, BoolVal
+from ..expressions.core import Comparison, Operator, BoolVal
 from ..expressions.variables import _BoolVarImpl, NegBoolView, boolvar
 from ..expressions.globalconstraints import DirectConstraint
+from ..transformations.linearize import canonical_comparison, only_positive_coefficients
 from ..expressions.utils import is_int, flatlist
 from ..transformations.decompose_global import decompose_in_tree
 from ..transformations.get_variables import get_variables
@@ -240,7 +241,6 @@ class CPM_pysat(SolverInterface):
         else:
             raise NotImplementedError(f"CPM_pysat: variable {cpm_var} not supported")
 
-
     def transform(self, cpm_expr):
         """
             Transform arbitrary CPMpy expressions to constraints the solver supports
@@ -261,6 +261,8 @@ class CPM_pysat(SolverInterface):
         cpm_cons = flatten_constraint(cpm_cons)
         cpm_cons = only_bv_reifies(cpm_cons)
         cpm_cons = only_implies(cpm_cons)
+        cpm_cons = canonical_comparison(cpm_cons)
+        cpm_cons = only_positive_coefficients(cpm_cons)
         return cpm_cons
 
     def __add__(self, cpm_expr_orig):
diff --git a/cpmpy/transformations/flatten_model.py b/cpmpy/transformations/flatten_model.py
index 4e654216..3b359c1b 100644
--- a/cpmpy/transformations/flatten_model.py
+++ b/cpmpy/transformations/flatten_model.py
@@ -215,12 +215,22 @@ def flatten_constraint(expr):
             lexpr, rexpr = expr.args
             rewritten = False
 
-            # rewrite 'Var == Expr' to normalzed 'Expr == Var'
-            if (expr.name == '==' or expr.name == '!=') \
-                    and __is_flat_var(lexpr) and not __is_flat_var(rexpr):
+            # rewrite 'Var # Expr' to normalized 'Expr # Var' (where # is any comparator)
+            if __is_flat_var(lexpr) and not __is_flat_var(rexpr):
+                assert (expr.name in ('==', '!=', '>', '>=', '<', '<='))
                 lexpr, rexpr = rexpr, lexpr
                 rewritten = True
 
+                # flip comparator in case of inequality
+                if exprname == '>':
+                    exprname = '<'
+                elif exprname == '>=':
+                    exprname = '<='
+                elif exprname == '<':
+                    exprname = '>'
+                elif exprname == '<=':
+                    exprname = '>='
+
             # already flat?
             if not expr.has_subexpr():
                 if not rewritten:
diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py
index c7314737..89773b9c 100644
--- a/cpmpy/transformations/linearize.py
+++ b/cpmpy/transformations/linearize.py
@@ -56,7 +56,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False):
     """
     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 'cpmpy.transformations.flatten_model.flatten_constraint()' 'and only_bv_implies()'.
+    Only apply after 'cpmpy.transformations.flatten_model.flatten_constraint()' 'and only_implies()'.
 
     `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_global()`
@@ -89,7 +89,7 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False):
                 # determine direction of implication
                 cond, sub_expr = cpm_expr.args
                 assert isinstance(cond, _BoolVarImpl), f"Linearization of {cpm_expr} is not supported, lhs of " \
-                                                       f"implication must be boolvar. Apply `only_bv_implies` before " \
+                                                       f"implication must be boolvar. Apply `only_implies` before " \
                                                        f"calling `linearize_constraint`"
 
                 if isinstance(cond, _BoolVarImpl) and isinstance(sub_expr, _BoolVarImpl):
@@ -285,7 +285,7 @@ def only_positive_bv(lst_of_expr):
             newlist += linearize_constraint(new_cons)
 
         # reification
-        elif cpm_expr.name == "->":
+        elif isinstance(cpm_expr, Operator) and cpm_expr.name == "->":
             cond, subexpr = cpm_expr.args
             assert isinstance(cond, _BoolVarImpl), f"{cpm_expr} is not a supported linear expression. Apply " \
                                                    f"`linearize_constraint` before calling `only_positive_bv` "
@@ -379,3 +379,49 @@ def canonical_comparison(lst_of_expr):
             newlist.append(cpm_expr)
 
     return newlist
+
+def only_positive_coefficients(lst_of_expr):
+    """
+        Replaces Boolean terms with negative coefficients in linear constraints with terms with positive coefficients 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.
+    """
+    newlist = []
+    for cpm_expr in lst_of_expr:
+        if isinstance(cpm_expr, Comparison):
+            lhs, rhs = cpm_expr.args
+
+            #    ... -c*b + ... <= k
+            # :: ... -c*(1 - ~b) + ... <= k
+            # :: ... -c + c* ~b + ... <= k
+            # :: ... + c*~b + ... <= k+c
+            if lhs.name == "wsum":
+                weights, args = lhs.args
+                idxes = {i for i, (w, a) in enumerate(zip(weights, args)) if w < 0 and isinstance(a, _BoolVarImpl)}
+                nw, na = zip(*[(-w, ~a) if i in idxes else (w, a) for i, (w, a) in enumerate(zip(weights, args))])
+                rhs += sum(-weights[i] for i in idxes)
+
+                # Simplify wsum to sum if all weights are 1
+                if all(w == 1 for w in nw):
+                    lhs = Operator("sum", [list(na)])
+                else:
+                    lhs = Operator("wsum", [list(nw), list(na)])
+
+            newlist.append(eval_comparison(cpm_expr.name, lhs, rhs))
+
+        # reification
+        elif isinstance(cpm_expr, Operator) and cpm_expr.name == "->":
+            cond, subexpr = cpm_expr.args
+            assert isinstance(cond, _BoolVarImpl), f"{cpm_expr} is not a supported linear expression. Apply " \
+                                                   f"`linearize_constraint` before calling `only_positive_coefficients` "
+            subexpr = only_positive_coefficients([subexpr])
+            newlist += [cond.implies(expr) for expr in subexpr]
+
+        else:
+            newlist.append(cpm_expr)
+
+    return newlist
+


Test patch:
diff --git a/tests/test_constraints.py b/tests/test_constraints.py
index 5a7a62e5..10b98b4c 100644
--- a/tests/test_constraints.py
+++ b/tests/test_constraints.py
@@ -126,21 +126,21 @@ def comp_constraints(solver):
         - Numeric disequality: Numexpr != Var              (CPMpy class 'Comparison')
                            Numexpr != Constant             (CPMpy class 'Comparison')
         - Numeric inequality (>=,>,<,<=): Numexpr >=< Var  (CPMpy class 'Comparison')
+                                          Var >=< NumExpr  (CPMpy class 'Comparison')
     """
-    for comp_name in Comparison.allowed:
+    for comp_name in sorted(Comparison.allowed):
 
         for numexpr in numexprs(solver):
             # numeric vs bool/num var/val (incl global func)
-            lb, ub = get_bounds(numexpr)
             for rhs in [NUM_VAR, BOOL_VAR, BoolVal(True), 1]:
                 if solver in SAT_SOLVERS and not is_num(rhs):
                     continue
-                if comp_name == ">" and ub <= get_bounds(rhs)[1]:
-                    continue
-                if comp_name == "<" and lb >= get_bounds(rhs)[0]:
-                    continue
-                yield Comparison(comp_name, numexpr, rhs)
-
+                for x,y in [(numexpr,rhs), (rhs,numexpr)]:
+                    # check if the constraint we are trying to construct is always UNSAT
+                    if any(eval_comparison(comp_name, xb,yb) for xb in get_bounds(x) for yb in get_bounds(y)):
+                        yield Comparison(comp_name, x, y)
+                    else: # impossible comparison, skip
+                        pass
 
 # Generate all possible boolean expressions
 def bool_exprs(solver):
@@ -271,7 +271,7 @@ def verify(cons):
 
 
 @pytest.mark.parametrize(("solver","constraint"),list(_generate_inputs(bool_exprs)), ids=str)
-def test_bool_constaints(solver, constraint):
+def test_bool_constraints(solver, constraint):
     """
         Tests boolean constraint by posting it to the solver and checking the value after solve.
     """
diff --git a/tests/test_pysat_cardinality.py b/tests/test_pysat_cardinality.py
index 1b193d2a..71c0824d 100644
--- a/tests/test_pysat_cardinality.py
+++ b/tests/test_pysat_cardinality.py
@@ -2,7 +2,9 @@ import unittest
 import pytest
 import cpmpy as cp 
 from cpmpy.expressions import *
+from cpmpy.expressions.core import Operator
 from cpmpy.solvers.pysat import CPM_pysat
+from cpmpy.transformations.linearize import only_positive_coefficients
 
 @pytest.mark.skipif(not CPM_pysat.supported(),
                     reason="PySAT not installed")
@@ -125,6 +127,36 @@ class TestCardinality(unittest.TestCase):
             cp.Model(c).solve("pysat")
             self.assertTrue(c.value())
 
+    def test_pysat_support_negative_coefficients(self):
+        bvs = cp.boolvar(3)
+        # this is linearized to `a+b-c>0`, which previously wasn't rewritten to the cardinality constraint `a+b+~c>1`
+        c = sum(bvs[1:]) > bvs[0]
+        s = cp.SolverLookup.get("pysat")
+        s += c
+        self.assertTrue(s.solve())
+
+    def test_pysat_aggregate_sum_sub_expressions(self):
+        bvs = cp.boolvar(3)
+        c = bvs[0] > sum(bvs[1:])
+        s = cp.SolverLookup.get("pysat")
+        s += c
+        self.assertTrue(s.solve())
+
+    def test_pysat_aggregate_sum_sub_expressions_implied(self):
+        bvs = cp.boolvar(3)
+        c = bvs[0] > sum(bvs[1:])
+        s = cp.SolverLookup.get("pysat")
+        s += c
+        self.assertTrue(s.solve())
+
+    def test_pysat_aggregate_sum_sub_expressions_implied(self):
+        a, b, c, p = [cp.boolvar(name=n) for n in "abcp"]
+        self.assertTrue(cp.SolverLookup.get("pysat", cp.Model(p.implies(a+b-c < 2))).solve())
+
+    @pytest.mark.skip(reason="TODO: PySAT does not linearize models at the moment, because there is no integer encoding layer, so adding non-linear expressions will always fail.")
+    def test_pysat_linearize_example(self):
+        self.assertTrue(cp.SolverLookup.get("pysat", cp.Model((a+b).implies(a+b-c < 2))).solve())
+
 
 if __name__ == '__main__':
     unittest.main()
diff --git a/tests/test_trans_linearize.py b/tests/test_trans_linearize.py
index 09bef43a..ad622cbd 100644
--- a/tests/test_trans_linearize.py
+++ b/tests/test_trans_linearize.py
@@ -3,7 +3,7 @@ import unittest
 import cpmpy as cp
 from cpmpy.expressions import boolvar, intvar
 from cpmpy.expressions.core import Operator
-from cpmpy.transformations.linearize import linearize_constraint, canonical_comparison
+from cpmpy.transformations.linearize import linearize_constraint, canonical_comparison, only_positive_coefficients
 from cpmpy.expressions.variables import _IntVarImpl, _BoolVarImpl
 
 
@@ -296,3 +296,17 @@ class testCanonical_comparison(unittest.TestCase):
         cons = canonical_comparison(cons)[0]
         self.assertEqual("alldifferent(a,b,c)", str(cons))
 
+    def test_only_positive_coefficients(self):
+        a, b, c = [cp.boolvar(name=n) for n in "abc"]
+        only_pos = only_positive_coefficients([Operator("wsum",[[1,1,-1],[a,b,c]]) > 0])
+        self.assertEqual(str([Operator("sum",[a, b, ~c]) > 1]), str(only_pos))
+
+    def test_only_positive_coefficients_implied(self):
+        a, b, c, p = [cp.boolvar(name=n) for n in "abcp"]
+        only_pos = only_positive_coefficients([p.implies(Operator("wsum",[[1,1,-1],[a,b,c]]) > 0)])
+        self.assertEqual(str([p.implies(Operator("sum",[a, b, ~c]) > 1)]), str(only_pos))
+
+    def test_only_positive_coefficients_pb_and_int(self):
+        a, b, c, x, y = [cp.boolvar(name=n) for n in "abc"] + [cp.intvar(0, 3, name=n) for n in "xy"]
+        only_pos = only_positive_coefficients([Operator("wsum",[[1,1,-1,1,-1],[a,b,c,x,y]]) > 0])
+        self.assertEqual(str([Operator("wsum",[[1,1,1,1,-1],[a,b,~c,x,y]]) > 1]), str(only_pos))