# /usr/bin/env python
"""
Interface to the Pindakaas solver's Python API.
Pindakaas is an open-source Rust library for encoding propositional and pseudo-Boolean constraints to SAT, with support for incremental solving and assumptions.
Always use :func:`cp.SolverLookup.get("pindakaas") <cpmpy.solvers.utils.SolverLookup.get>` to instantiate the solver object.
============
Installation
============
Requires that the 'pindakaas' optional dependency is installed:
.. code-block:: console
$ pip install pindakaas
Detailed installation instructions available at:
- https://pypi.org/project/pindakaas/
- https://github.com/pindakaashq/pindakaas
The rest of this documentation is for advanced users.
===============
List of classes
===============
.. autosummary::
:nosignatures:
CPM_pindakaas
==============
Module details
==============
"""
import time
from datetime import timedelta
from typing import Iterable, Optional, List, Any
from ..exceptions import NotSupportedError
from ..expressions.core import Expression, BoolVal, Comparison, NestedBoolExprLike
from ..expressions.utils import eval_comparison, is_int
from ..expressions.variables import NegBoolView, _BoolVarImpl, _NumVarImpl
from ..transformations.flatten_model import flatten_constraint
from ..transformations.get_variables import get_variables
from ..transformations.int2bool import _decide_encoding, _encode_int_var, int2bool
from ..transformations.linearize import linearize_constraint, linearize_reified_variables, decompose_linear
from ..transformations.normalize import simplify_boolean, toplevel_list
from ..transformations.negation import push_down_negation
from ..transformations.reification import only_bv_reifies, only_implies
from ..transformations.safening import no_partial_functions
from .solver_interface import ExitStatus, SolverInterface
[docs]
class CPM_pindakaas(SolverInterface):
"""
Interface to Pindakaas' Python API.
Creates the following attributes (see parent constructor for more):
- ``pdk_solver``: The Pindakaas solver back-end which encodes and solves models through the SAT sub-solver
- ``ivarmap``: a mapping from integer variables to their encoding for `int2bool`
- ``encoding``: the encoding used for `int2bool`, choose from ("auto", "direct", "order", or "binary"). Set to "auto" but can be changed in the solver object.
- `unsatisfiable`: if a constraint is found to be unsatisfiable during the encoding phase, this flag is set to `True` to prevent further encoding efforts
- ``core``: if the problem is unsatisfiable, the unsatisfiable core, else `None`
Documentation of the solver's own Python API:
- https://pypi.org/project/pindakaas/
- https://github.com/pindakaashq/pindakaas
"""
supported_global_constraints = frozenset()
supported_reified_global_constraints = frozenset()
[docs]
@staticmethod
def supported():
try:
import pindakaas
return True
except ModuleNotFoundError:
return False
[docs]
@staticmethod
def version() -> Optional[str]:
"""Return the installed version of the solver's Python API."""
from importlib.metadata import PackageNotFoundError, version
try:
return version("pindakaas")
except PackageNotFoundError:
return None
def __init__(self, cpm_model=None, subsolver=None):
"""
Initialize Pindakaas interface.
"""
name = "pindakaas"
if not self.supported():
raise ModuleNotFoundError(f"CPM_{name}: Install the python package 'cpmpy[pindakaas]' to use this solver interface.")
if cpm_model and cpm_model.objective_ is not None:
raise NotSupportedError(f"CPM_{name}: only satisfaction, does not support an objective function")
import pindakaas as pdk
assert subsolver is None, "Pindakaas does not support any subsolvers for the moment"
self.ivarmap = dict() # for the integer to boolean encoders
self.encoding = "auto"
self.pdk_solver = pdk.solver.CaDiCaL()
self.unsatisfiable = False # `pindakaas` might determine unsat before solving
self.core = None # latest UNSAT core
super().__init__(name=name, cpm_model=cpm_model)
@property
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
[docs]
def solve(self, time_limit: Optional[float] = None, assumptions: Optional[Iterable[_BoolVarImpl]] = None):
"""
Solve the encoded CPMpy model given optional time limit and assumptions, returning whether a solution was found.
:param time_limit: optional, time limit in seconds
:param assumptions: optional, an iterable (e.g. list, set, tuple) of assumptions (Boolean variables which should hold for this solve call)
"""
if self.unsatisfiable:
self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
return self._solve_return(self.cpm_status)
if time_limit is not None and time_limit <= 0:
raise ValueError("Time limit must be positive")
self.user_vars = self._int2bool_user_vars()
time_limit_delta: Optional[timedelta] = None
if time_limit is not None:
time_limit_delta = timedelta(seconds=time_limit)
if assumptions is not None:
assumptions = list(assumptions) # iterable to ordered list
solver_assumptions = self.solver_vars(assumptions)
else:
solver_assumptions = None
t = time.time()
with self.pdk_solver.solve(time_limit=time_limit_delta, assumptions=solver_assumptions) as result:
self.cpm_status.runtime = time.time() - t
# translate pindakaas result status to cpmpy status
import pindakaas as pdk
if result.status == pdk.solver.Status.SATISFIED:
self.cpm_status.exitstatus = ExitStatus.FEASIBLE
elif result.status == pdk.solver.Status.UNSATISFIABLE:
self.cpm_status.exitstatus = ExitStatus.UNSATISFIABLE
elif result.status == pdk.solver.Status.UNKNOWN:
self.cpm_status.exitstatus = ExitStatus.UNKNOWN
else:
raise NotImplementedError(f"Pindakaas returned an unkown type of result status: {result}")
# True/False depending on self.cpm_status
has_sol = self._solve_return(self.cpm_status)
# translate solution values (of user specified variables only)
if has_sol:
# fill in variable values
for cpm_var in self.user_vars:
# essentially `.solver_var`, but failing if new vars are added
if isinstance(cpm_var, NegBoolView):
lit = ~self._varmap[cpm_var._bv.name]
elif isinstance(cpm_var, _BoolVarImpl):
lit = self._varmap[cpm_var.name]
else:
raise ValueError(
f"Integer variables should have been encoded using `int2bool` transformation, but {cpm_var} is integer, please report on GitHub"
)
value = result.value(lit)
assert value is not None, (
f"All user variables should have been assigned, but {cpm_var} (literal {lit}) was not."
)
cpm_var._value = value
self.core = None
# Now assign the user integer variables using their encodings
# `ivarmap` also contains auxiliary variable, but they will be assigned 'None' as their encoding variables are assigned `None`
for enc in self.ivarmap.values():
enc._x._value = enc.decode()
else: # clear values of variables
for cpm_var in self.user_vars:
cpm_var._value = None
for enc in self.ivarmap.values():
enc._x._value = None
# we have to save the unsat core here, as the result object does not live beyond this solve call
if assumptions is not None:
assert solver_assumptions is not None and len(assumptions) == len(solver_assumptions), "Number of assumptions and solver assumptions must match"
self.core = [x for x, s_x in zip(assumptions, solver_assumptions) if result.failed(s_x)]
return has_sol
[docs]
def solver_var(self, cpm_var):
"""
Creates solver variable for cpmpy variable
or returns from cache if previously created
or returns a constant if the variable is a constant
"""
if isinstance(cpm_var, _NumVarImpl):
name = cpm_var.name
revar = self._varmap.get(name)
if revar is not None:
return revar
if cpm_var.is_bool():
if isinstance(cpm_var, NegBoolView): # negative literal
# get inner variable and return its negated solver var
revar = ~self.solver_var(cpm_var._bv)
else:
revar = self.pdk_solver.new_var()
else:
if name not in self.ivarmap:
enc, cons = _encode_int_var(self.ivarmap, cpm_var, _decide_encoding(cpm_var, None, encoding=self.encoding))
self.add(cons)
else:
enc = self.ivarmap[name]
revar = self.solver_vars(enc.vars())
self._varmap[name] = revar
return revar
if is_int(cpm_var): # shortcut, eases posting constraints
return cpm_var
raise TypeError(f"Unexpected type: {cpm_var}")
[docs]
def add(self, cpm_expr: NestedBoolExprLike) -> "CPM_pindakaas":
"""
Eagerly add a constraint to the underlying solver.
Any CPMpy expression given is immediately transformed (through `transform()`)
and then posted to the solver in this function.
This can raise 'NotImplementedError' for any constraint not supported after transformation
The variables used in expressions given to add are stored as 'user variables'. Those are the only ones
the user knows and cares about (and will be populated with a value after solve). All other variables
are auxiliary variables created by transformations.
Arguments:
cpm_expr (NestedBoolExprLike): CPMpy expression, or list thereof
Returns:
self
"""
import pindakaas as pdk
if self.unsatisfiable:
return self
# add new user vars to the set
get_variables(cpm_expr, collect=self.user_vars)
# transform and post the constraints
try:
for con in self.transform(cpm_expr):
self._post_constraint(con)
except pdk.Unsatisfiable:
self.unsatisfiable = True
return self
__add__ = add # avoid redirect in superclass
def _add_clause(self, clause, conditions=[]):
"""Add a clause implied by conditions; both arguments are lists of CPMpy literals."""
if not isinstance(clause, (tuple, list)):
raise TypeError
self.pdk_solver.add_clause(self.solver_vars([~c for c in conditions] + list(clause)))
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._add_clause([], conditions=conditions)
elif isinstance(cpm_expr, _BoolVarImpl): # (implied) literal
self._add_clause([cpm_expr], conditions=conditions)
elif cpm_expr.name == "or": # (implied) clause
self._add_clause(cpm_expr.args, conditions=conditions)
elif cpm_expr.name == "->": # implication
a0, a1 = cpm_expr.args
self._post_constraint(a1, conditions=conditions + [a0])
elif isinstance(cpm_expr, Comparison): # Bool linear
assert cpm_expr.name in {"<=", ">=", "=="}, (
f"Unsupported comparator {cpm_expr.name} for constraint should have been transformed: {cpm_expr}"
)
# lhs is a sum/wsum, right hand side a constant int
lhs, rhs = cpm_expr.args
if isinstance(lhs, _BoolVarImpl):
literals = [lhs]
coefficients = [1]
elif lhs.name == "sum":
literals = lhs.args
coefficients = [1] * len(literals)
elif lhs.name == "wsum":
coefficients, literals = lhs.args
else:
raise ValueError(f"Trying to encode non (Boolean) linear constraint: {cpm_expr}")
# Create `pindakaas` Boolean linear expression object
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=self.solver_vars(conditions))
else:
raise NotSupportedError(f"{self.name}: Unsupported constraint {cpm_expr}")
[docs]
def get_core(self):
assert self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE and self.core is not None, (
"get_core(): requires a previous solve call with assumption variables and an UNSATISFIABLE result"
)
return self.core