Expand CNF using encoding back-end

cpmpy/solvers/pindakaas.py

@@ -121,6 +121,20 @@ def __init__(self, cpm_model=None, subsolver=None):
     def native_model(self):
         return self.pdk_solver
 
+    def _int2bool_user_vars(self):
+        # ensure all vars are known to solver
+        self.solver_vars(list(self.user_vars))
+
+        # the user vars are only the Booleans (e.g. to ensure solveAll behaves consistently)
+        user_vars = set()
+        for x in self.user_vars:
+            if isinstance(x, _BoolVarImpl):
+                user_vars.add(x)
+            else:
+                # extends set with encoding variables of `x`
+                user_vars.update(self.ivarmap[x.name].vars())
+        return user_vars
+
     def solve(self, time_limit=None, assumptions=None):
         """
         Solve the encoded CPMpy model given optional time limit and assumptions, returning whether a solution was found.
@@ -135,19 +149,7 @@ def solve(self, time_limit=None, assumptions=None):
         if time_limit is not None and time_limit <= 0:
             raise ValueError("Time limit must be positive")
 
-        # ensure all vars are known to solver
-        self.solver_vars(list(self.user_vars))
-
-        # the user vars are only the Booleans (e.g. to ensure solveAll behaves consistently)
-        user_vars = set()
-        for x in self.user_vars:
-            if isinstance(x, _BoolVarImpl):
-                user_vars.add(x)
-            else:
-                # extends set with encoding variables of `x`
-                user_vars.update(self.ivarmap[x.name].vars())
-
-        self.user_vars = user_vars
+        self.user_vars = self._int2bool_user_vars()
 
         if time_limit is not None:
             time_limit = timedelta(seconds=time_limit)
@@ -263,22 +265,33 @@ def add(self, cpm_expr_orig):
 
     __add__ = add  # avoid redirect in superclass
 
+    def _add_clause(self, cpm_expr):
+        if not isinstance(cpm_expr, list):
+            raise TypeError
+
+        self.pdk_solver.add_clause(self.solver_vars(cpm_expr))
+
     def _post_constraint(self, cpm_expr, conditions=[]):
+        if not isinstance(conditions, list):
+            raise TypeError
+
         """Add a single, *transformed* constraint, implied by conditions."""
         if isinstance(cpm_expr, BoolVal):
             # base case: Boolean value
             if cpm_expr.args[0] is False:
-                self.pdk_solver.add_clause(conditions)
+                self._add_clause(conditions)
 
         elif isinstance(cpm_expr, _BoolVarImpl):  # (implied) literal
-            self.pdk_solver.add_clause(conditions + [self.solver_var(cpm_expr)])
+            self._add_clause(conditions + [cpm_expr])
 
         elif cpm_expr.name == "or":  # (implied) clause
-            self.pdk_solver.add_clause(conditions + self.solver_vars(cpm_expr.args))
+            self._add_clause(conditions + cpm_expr.args)
 
         elif cpm_expr.name == "->":  # implication
             a0, a1 = cpm_expr.args
-            self._post_constraint(a1, conditions=conditions + [~self.solver_var(a0)])
+            if not isinstance(a0, _BoolVarImpl):
+                raise TypeError
+            self._post_constraint(a1, conditions=conditions + [~a0])
 
         elif isinstance(cpm_expr, Comparison):  # Bool linear
             assert cpm_expr.name in {"<=", ">=", "=="}, (
@@ -300,7 +313,9 @@ def _post_constraint(self, cpm_expr, conditions=[]):
 
             lhs = sum(c * l for c, l in zip(coefficients, self.solver_vars(literals)))
 
-            self.pdk_solver.add_encoding(eval_comparison(cpm_expr.name, lhs, rhs), conditions=conditions)
+            self.pdk_solver.add_encoding(
+                eval_comparison(cpm_expr.name, lhs, rhs), conditions=self.solver_vars(conditions)
+            )
         else:
             raise NotSupportedError(f"{self.name}: Unsupported constraint {cpm_expr}")
 

cpmpy/transformations/to_cnf.py

@@ -1,82 +1,68 @@
 """
-  Meta-transformation for obtaining a CNF from a list of constraints.
-
-  Converts the logical constraints into disjuctions using the tseitin transform,
-  including flattening global constraints that are :func:`~cpmpy.expressions.core.Expression.is_bool()` and not in `supported`.
-
-  .. note::
-    The transformation is no longer used by the SAT solvers, and may be outdated.
-    Check :meth:`CPM_pysat.transform <cpmpy.solvers.pysat.CPM_pysat.transform>` for an up-to-date alternative.
-
-  Other constraints are copied verbatim so this transformation
-  can also be used in non-pure CNF settings.
-
-  The implementation first converts the list of constraints
-  to **Flat Normal Form**, this already flattens subexpressions using
-  auxiliary variables.
+Transform constraints to **Conjunctive Normal Form** (i.e. an `and` of `or`s of literals, i.e. Boolean variables or their negation, e.g. from `x xor y` to `(x or ~y) and (~x or y)`) using a back-end encoding library and its transformation pipeline.
+"""
 
-  What is then left to do is to tseitin encode the following into CNF:
+import cpmpy as cp
+from ..solvers.pindakaas import CPM_pindakaas
+from ..transformations.get_variables import get_variables
 
-  - ``BV`` with BV a ``BoolVar`` (or ``NegBoolView``)
-  - ``or([BV])`` constraint
-  - ``and([BV])`` constraint
-  - ``BE != BV``  with ``BE :: BV|or()|and()|BV!=BV|BV==BV|BV->BV``
-  - ``BE == BV``
-  - ``BE -> BV``
-  - ``BV -> BE``
-"""
-from ..expressions.core import Operator
-from ..expressions.variables import _BoolVarImpl
-from .reification import only_implies
-from .flatten_model import flatten_constraint
 
-def to_cnf(constraints, csemap=None):
+def to_cnf(constraints, csemap=None, ivarmap=None):
     """
-        Converts all logical constraints into **Conjunctive Normal Form**
+    Converts all constraints into **Conjunctive Normal Form**
 
-        Arguments:
-            constraints:    list[Expression] or Operator
-            supported:      (frozen)set of global constraint names that do not need to be decomposed
+    Arguments:
+        constraints:    list[Expression] or Operator
+        csemap:         `dict()` used for CSE
+        ivarmap:        `dict()` used to map integer variables to their encoding (usefull for finding the values of the now-encoded integer variables)
+    Returns:
+        Equivalent CPMpy constraints in CNF, and the updated `ivarmap`
     """
-    fnf = flatten_constraint(constraints, csemap=csemap)
-    fnf = only_implies(fnf, csemap=csemap)
-    return flat2cnf(fnf)
+    if not CPM_pindakaas.supported():
+        raise ImportError(
+            f"Install the Pindakaas python library `pindakaas` (e.g. `pip install pindakaas`) package to use the `to_cnf` transformation"
+        )
 
-def flat2cnf(constraints):
-    """
-        Converts from **Flat Normal Form** all logical constraints into **Conjunctive Normal Form**,
-        including flattening global constraints that are :func:`~cpmpy.expressions.core.Expression.is_bool()` and not in `supported`.
+    import pindakaas as pdk
 
-        What is now left to do is to tseitin encode:
+    slv = CPM_pindakaas()
+    if ivarmap is not None:
+        slv.ivarmap = ivarmap
+    slv._csemap = csemap
 
-        - ``BV`` with BV a ``BoolVar`` (or ``NegBoolView``)
-        - ``or([BV])`` constraint
-        - ``and([BV])`` constraint
-        - ``BE != BV``  with ``BE :: BV|or()|and()|BV!=BV|BV==BV|BV->BV``
-        - ``BE == BV``
-        - ``BE -> BV``
-        - ``BV -> BE``
+    # the encoded constraints (i.e. `PB`s) will be added to this `pdk.CNF` object
+    slv.pdk_solver = pdk.CNF()
 
-        We do it in a principled way for each of the cases. (in)equalities
-        get transformed into implications, everything is modular.
+    # however, we bypass `pindakaas` for simple clauses
+    clauses = []
+    slv._add_clause = lambda cpm_expr: clauses.append(cp.any(cpm_expr))
 
-        Arguments:
-            constraints: list[Expression] or Operator
-    """
-    cnf = []
-    for expr in constraints:
-        # BE -> BE
-        if expr.name == '->':
-            a0,a1 = expr.args
+    # add, transform, and encode constraints into CNF/clauses
+    slv += constraints
+
+    # now we read the pdk.CNF back to cpmpy constraints by mapping from `pdk.Lit` to CPMpy lit
+    cpmpy_vars = {str(slv.solver_var(x).var()): x for x in slv._int2bool_user_vars()}
+
+    # if a user variable `x` does not occur in any clause, they should be added as `x | ~x`
+    free_vars = set(cpmpy_vars.values()) - set(get_variables(clauses))
 
-            # BoolVar() -> BoolVar()
-            if isinstance(a1, _BoolVarImpl) or \
-                    (isinstance(a1, Operator) and a1.name == 'or'):
-                cnf.append(~a0 | a1)
-                continue
+    def to_cpmpy_clause(clause):
+        """Lazily convert `pdk.CNF` to CPMpy."""
+        for lit in clause:
+            x = str(lit.var())
+            if x not in cpmpy_vars:
+                cpmpy_vars[x] = cp.boolvar()
+            y = cpmpy_vars[x]
+            try:
+                free_vars.remove(y)
+            except KeyError:
+                pass
+            if lit.is_negated():
+                yield ~y
+            else:
+                yield y
 
-        # all other cases added as is...
-        # TODO: we should raise here? is not really CNF...
-        cnf.append(expr)
+    clauses += (cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses())
+    clauses += ((x | ~x) for x in free_vars)  # add free variables so they are "known" by the CNF
 
-    return cnf
+    return clauses

tests/test_tocnf.py

@@ -1,76 +1,91 @@
 import unittest
-import numpy as np
-from cpmpy import *
-from cpmpy.solvers import CPM_ortools
+import cpmpy as cp
+
+
 from cpmpy.transformations.to_cnf import to_cnf
 from cpmpy.transformations.get_variables import get_variables
-from cpmpy.expressions.core import Operator
 from cpmpy.expressions.globalconstraints import Xor
+from cpmpy.expressions.utils import argvals
+from cpmpy.solvers.pindakaas import CPM_pindakaas
+
+import pytest
+
 
+@pytest.mark.skipif(not CPM_pindakaas.supported(), reason="Pindakaas (required for `to_cnf`) not installed")
 class TestToCnf(unittest.TestCase):
     def test_tocnf(self):
-        a,b,c = boolvar(shape=3)
+        a, b, clause = cp.boolvar(shape=3)
+        x = cp.intvar(1, 2)
+        y, z = cp.intvar(0, 1, shape=2)
 
-        cases = [a,
-                 a|b,
-                 a&b,
-                 a!=b,
-                 a==b,
-                 a.implies(b),
-                 a.implies(b|c),
-                 a.implies(b&c),
-                 a.implies(b!=c),
-                 a.implies(b==c),
-                 a.implies(b.implies(c)),
-                 (b|c).implies(a),
-                 (b&c).implies(a),
-                 (b!=c).implies(a),
-                 (b==c).implies(a),
-                 (b.implies(c)).implies(a),
-                 Xor([a,b]),
-                ]
+        bvs = cp.boolvar(shape=3)
+        cases = [
+            a,
+            a | b,
+            a & b,
+            a != b,
+            a == b,
+            a.implies(b),
+            a.implies(b | clause),
+            a.implies(b & clause),
+            a.implies(b != clause),
+            a.implies(b == clause),
+            a.implies(b.implies(clause)),
+            (b | clause).implies(a),
+            (b & clause).implies(a),
+            (b != clause).implies(a),
+            (b == clause).implies(a),
+            (b.implies(clause)).implies(a),
+            Xor([a, b]),
+            cp.sum([2 * x + 3 * y]) <= 4,
+            cp.sum([2 * x + 3 * y + 5 * z]) <= 6,
+            cp.sum([2 * cp.intvar(1, 2) + 3 * cp.intvar(0, 1)]) <= 4,
+            cp.sum([3 * cp.intvar(0, 1)]) <= 4,
+            (a + b + clause) == 1,
+            # a * b == 1,  # TODO in linearization!
+            # a * b != 1,
+            (a + b + clause) != 1,
+            a + b + clause > 2,
+            a + b + clause <= 2,
+            cp.sum(cp.intvar(lb=2, ub=3, shape=3)) <= 3,
+        ]
 
         # test for equivalent solutions with/without to_cnf
         for case in cases:
-            vs = cpm_array(get_variables(case))
+            vs = cp.cpm_array(get_variables(case))
             s1 = self.allsols([case], vs)
-            s1.sort(axis=0)
-            s2 = self.allsols(to_cnf(case), vs)
-            s2.sort(axis=0)
-            for ss1,ss2 in zip(s1,s2):
-                self.assertTrue(np.all(ss1 == ss2), (case, s1, s2))
+            ivarmap = dict()
+            cnf = to_cnf(case, ivarmap=ivarmap)
 
-        # test for errors in edge cases of to_cnf
-        bvs = boolvar(shape=3)
-        ivs = intvar(lb=2, ub=3, shape=3)
-        edge_cases = [
-            # do not consider object as a double implcation, but as a sum
-            (a + b + c) == 1,
-            a * b == 1,
-            a * b != 1,
-            (a + b + c) != 1,
-            sum(bvs) > 2,
-            sum(bvs) <= 2,
-            sum(ivs) <= 3
-        ]
+            # TODO
+            # assert (
+            #     cnf is False
+            #     or isinstance(cnf, _BoolVarImpl)
+            #     or cnf.name == "and"
+            #     and all(
+            #         clause.name == "or"
+            #         and all([is_bool(lit) or isinstance(lit, _BoolVarImpl) for lit in clause.args])
+            #         for clause in cnf.args
+            #     )
+            # ), f"The following was not CNF: {cnf}"
 
-        # check for error in edge cases
-        for case in edge_cases:
-            cnf = to_cnf(case)
-            # Expressions should not be decomposed at the to_cnf level!
-            self.assertEqual(len(cnf), 1)
+            s2 = self.allsols(cnf, vs, ivarmap=ivarmap)
+            assert s1 == s2, f"The equivalence check failed for translaton from {case} to {cnf}"
 
-    def allsols(self, cons, vs):
-        sols = []
+    def allsols(self, cons, vs, ivarmap=None):
+        m = cp.Model(cons)
+        sols = set()
 
-        m = CPM_ortools(Model(cons))
-        while m.solve():
-            sols.append(vs.value())
-            m += ~all(vs == vs.value())
+        def display():
+            if ivarmap:
+                for x_enc in ivarmap.values():
+                    x_enc._x._value = x_enc.decode()
+            sols.add(tuple(argvals(vs)))
 
-        return np.array(sols)
+        m.solveAll(solver="ortools", display=display, solution_limit=100)
+        assert len(sols) < 100, sols
+        return sols
 
 
-if __name__ == '__main__':
+if __name__ == "__main__":
     unittest.main()
-

tests/test_tool_dimacs.py

@@ -7,7 +7,11 @@
 from cpmpy.tools.dimacs import read_dimacs, write_dimacs
 from cpmpy.transformations.get_variables import get_variables_model
 from cpmpy.solvers.solver_interface import ExitStatus
+from cpmpy.solvers.pindakaas import CPM_pindakaas
 
+
+
+@pytest.mark.skipif(not CPM_pindakaas.supported(), reason="Pindakaas (required for `to_cnf`) not installed")
 class CNFTool(unittest.TestCase):
 
     def setUp(self) -> None:
@@ -60,7 +64,8 @@ def test_write_cnf(self):
         m += a <= 0
 
         cnf_txt = write_dimacs(m)
-        gt_cnf = "p cnf 3 3\n1 2 3 0\n-2 -3 0\n-1 0\n"
+        # TODO note the order is slightly unexpected, because of an optimization in `to_cnf` which puts simple clauses before encoded constraints (i.e.) sums
+        gt_cnf = "p cnf 3 3\n1 2 3 0\n-1 0\n-2 -3 0\n"
 
         self.assertEqual(cnf_txt, gt_cnf)