CPMpy rc2 interface (cpmpy.solvers.rc2)

Interface to PySAT’s RC2 MaxSAT solver API

PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified interface to a number of state-of-art Boolean satisfiability (SAT) solvers. It also includes the RC2 MaxSAT solver. (see https://pysathq.github.io/)

Warning

It does not support satisfaction, only optimization.

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

Installation

Requires that the ‘python-sat’ package is installed:

$ pip install pysat

If you want to also solve pseudo-Boolean constraints, you should also install its optional dependency ‘pypblib’, as follows:

$ pip install pypblib

See detailed installation instructions at: https://pysathq.github.io/installation

The rest of this documentation is for advanced users.

List of classes

CPM_rc2

Interface to PySAT's RC2 MaxSAT solver API.

Module details

class cpmpy.solvers.rc2.CPM_rc2(cpm_model=None, subsolver=None)[source]

Interface to PySAT’s RC2 MaxSAT solver API.

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

  • pysat_vpool: a pysat.formula.IDPool for the variable mapping

  • pysat_solver: a pysat.examples.rc2.RC2() (or .RC2Stratified())

  • 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.

The DirectConstraint, when used, calls a function on the pysat_solver object.

Documentation of the solver’s own Python API: https://pysathq.github.io/docs/html/api/examples/rc2.html

Note

CPMpy uses ‘model’ to refer to a constraint specification, the PySAT docs use ‘model’ to refer to a solution.

add(cpm_expr_orig)

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.

What ‘supported’ means depends on the solver capabilities, and in effect on what transformations are applied in transform().

get_core()

For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.

CPMpy will return only those assumptions which are False (in the UNSAT core)

Note that there is no guarantee that the core is minimal. More advanced Minimal Unsatisfiable Subset are available in the ‘examples’ folder on GitHub

has_objective()[source]

Returns whether the solver has an objective function or not.

maximize(expr)

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)

Post the given expression to the solver as objective to minimize

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

property native_model

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

objective(expr, minimize)[source]

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

Parameters:

  • expr – Expression, the CPMpy expression that represents the objective function

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

objective_value()

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

solution_hint(cpm_vars: List[_BoolVarImpl], vals: List[bool])

PySAT supports warmstarting the solver with a feasible solution

In PySAT, this is called setting the ‘phases’ or the ‘polarities’ of literals

Note: our PySAT interface currently does not support solution hinting for integer variables

Parameters:

  • cpm_vars – list of CPMpy variables

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

solve(time_limit=None, **kwargs)[source]

Call the RC2 MaxSAT solver

Parameters:

time_limit (float, optional) –

Maximum solve time in seconds. Auto-interrups in case the runtime exceeds given time_limit.

Warning

Warning: the time_limit is not very accurate at subsecond level

The following **kwargs are supported for RC2:

stratified (bool, optional): use the stratified solver for weighted maxsat (default: True) adapt (bool, optional): detect and adapt intrinsic AtMost1 constraint (default: True) exhaust (bool, optional): do core exhaustion (default: True) minz (bool, optional): do heuristic core reduction (default: True)

If no **kwargs are given, the default values are used as recommended by the PySAT authors, based on their MaxSAT Evaluation 2018 submission, i.e.: {“solver”: “glucose3”, “adapt”: True, “exhaust”: True, “minz”: True}. If **kwargs are given, these are passed to RC2. Note that currently, no args are passed to the underlying oracle.

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

Compute all solutions and optionally display the solutions.

This is the generic implementation, solvers can overwrite this with a more efficient native implementation

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 (-) – stop after this many seconds (default: None)

  • solution_limit (-) – stop after this many solutions (default: None)

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

  • argument (- any other keyword)

Returns:

number of solutions found

solver_var(cpm_var)

Creates solver variable for cpmpy variable or returns from cache if previously created.

Transforms cpm_var into CNF literal using self.pysat_vpool (positive or negative integer).

So vpool is the varmap (we don’t use _varmap here).

solver_vars(cpm_vars)

Like solver_var() but for arbitrary shaped lists/tensors

static solvernames(**kwargs)

Returns solvers supported by PySAT on your system

static solverversion(subsolver: str) → str | None

Returns the version of the requested subsolver.

Parameters:

subsolver (str) – name of the subsolver

Returns:

Version number of the subsolver if installed, else None

Pysat currently does not provide accessible subsolver version numbers.

status()
static supported()

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({})
supported_reified_global_constraints: frozenset[str] = frozenset({})
transform(cpm_expr)

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.

In the case of PySAT, the supported constraints are over Boolean variables:

  • Boolean clauses

  • Cardinality constraint (sum)

  • Pseudo-Boolean constraints (wsum)

Parameters:

cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof

Returns:

list of Expression

transform_objective(expr)[source]

Transform the objective to a list of (w,x) and a constant

static version() → str | None

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