CPMpy pysdd interface (cpmpy.solvers.pysdd)

Interface to PySDD’s API

PySDD is a knowledge compilation package for Sentential Decision Diagrams (SDD). (see https://pysdd.readthedocs.io/en/latest/)

Warning

This solver can ONLY be used for solution checking and enumeration over Boolean variables! It does not support optimization.

Always use cp.SolverLookup.get("pysdd") to instantiate the solver object.

Installation

Requires that the ‘PySDD’ python package is installed:

$ pip install PySDD

See detailed installation instructions at: https://pysdd.readthedocs.io/en/latest/usage/installation.html

The rest of this documentation is for advanced users.

List of classes

CPM_pysdd

Interface to PySDD's API.

Module details

class cpmpy.solvers.pysdd.CPM_pysdd(cpm_model=None, subsolver=None)[source]

Interface to PySDD’s API.

Creates the following attributes (see parent constructor for more):

  • pysdd_vtree : a pysdd.sdd.Vtree

  • pysdd_manager : a pysdd.sdd.SddManager

  • pysdd_root : a pysdd.sdd.SddNode (changes whenever a formula is added)

The DirectConstraint, when used, calls a function on the pysdd_manager object and replaces the root node with a conjunction of the previous root node and the result of this function call.

Documentation of the solver’s own Python API: https://pysdd.readthedocs.io/en/latest/classes/SddManager.html

add(cpm_expr: Expression | bool | bool | Sequence[Expression | bool | bool | Sequence[NestedBoolExprLike] | ndarray] | ndarray) → CPM_pysdd[source]

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.

Parameters:

cpm_expr (NestedBoolExprLike) – CPMpy expression, or list thereof

Returns:

self

dot()[source]

Returns a graphviz Dot object

Display (in a notebook) with:

import graphviz
graphviz.Source(m.dot())
get_core()

For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT.

Typically implemented in SAT-based solvers

Returns a small subset of assumption literals that are unsat together. (a literal is either a _BoolVarImpl or a NegBoolView in case of its negation, e.g. x or ~x) Setting these literals to True makes the model UNSAT, setting any to False makes it SAT

has_objective() → bool

Returns whether the solver has an objective function or not.

maximize(expr: Expression) → None

Post the given expression to the solver as objective to maximize

maximize() can be called multiple times, only the last one is stored

minimize(expr: Expression) → None

Post the given expression to the solver as objective to minimize

minimize() can be called multiple times, only the last one is stored

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

  • soft – List of soft constraints over which a MUS needs to be found

  • hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model

Returns the solver’s underlying native model (for direct solver access).

objective(expr: Expression, minimize: bool) → None

Post the given expression to the solver as objective to minimize/maximize

Parameters:

  • expr – a CPMpy Expression

  • minimize – Bool, whether it is a minimization problem (True) or maximization problem (False)

objective() can be called multiple times, only the last one is stored

objective_value() → int | None

Returns the value of the objective function of the latest solver run on this model

Returns:

an integer or ‘None’ if it is not run, or a satisfaction problem

objective_value_: int | None
print_display(display: Expression | Sequence[Expression] | ndarray | Callable[[], None] | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:

display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

solution_hint(cpm_vars: List[_NumVarImpl], vals: List[int | bool])

For warmstarting the solver with a variable assignment

Typically implemented in SAT-based solvers

Parameters:

  • cpm_vars – list of CPMpy variables

  • vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None)[source]

See if an arbitrary model exists

This is a knowledge compiler:

  • building it is the (computationally) hard part

  • checking for a solution is trivial after that

solveAll(display: Expression | Sequence[Expression] | ndarray | Callable[[], None] | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]

Compute all solutions and optionally display the solutions.

Warning

WARNING: setting ‘display’ will SIGNIFICANTLY slow down solution counting…

Parameters:

  • display (-) – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping default/None: nothing displayed

  • time_limit (-) – not used

  • solution_limit – not used

  • kwargs – not used

  • call_from_model (-) – whether the method is called from a CPMpy Model instance or not

Returns:

number of solutions found

solver_var(cpm_var)[source]

Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]

Like solver_var() but for arbitrary shaped lists/tensors

status()
static supported()[source]

Check for support in current system setup. Return True if the system has package installed or supports solver, else returns False.

Returns:

Solver support by current system setup.

Return type:

[bool]

supported_global_constraints: frozenset[str] = frozenset({'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({'xor'})
transform(cpm_expr: Expression | bool | bool | Sequence[Expression | bool | bool | Sequence[NestedBoolExprLike] | ndarray] | ndarray) → list[Expression][source]

Transform arbitrary CPMpy expressions to constraints the solver supports

Implemented through chaining multiple solver-independent transformation functions from the cpmpy/transformations/ directory.

See the ‘Adding a new solver docs on readthedocs for more information.

For PySDD, it can be beneficial to add a big model (collection of constraints) at once…

Parameters:

cpm_expr (NestedBoolExprLike) – CPMpy expression, or list thereof

Returns:

transformed constraints

Return type:

list[Expression]

static version() → str | None[source]

Returns the installed version of the solver’s Python API.