diff --git a/cpmpy/solvers/pindakaas.py b/cpmpy/solvers/pindakaas.py index 20540903a..051731513 100755 --- a/cpmpy/solvers/pindakaas.py +++ b/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}") diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 5a03f28e2..66cb3314b 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/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 ` 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 diff --git a/tests/test_tocnf.py b/tests/test_tocnf.py index eefef07bb..efdd1048c 100644 --- a/tests/test_tocnf.py +++ b/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() - diff --git a/tests/test_tool_dimacs.py b/tests/test_tool_dimacs.py index 57e43f587..8b7c28944 100644 --- a/tests/test_tool_dimacs.py +++ b/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)