CPMpy pysat interface (cpmpy.solvers.pysat
)
Interface to PySAT’s 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 as well as to a variety of cardinality and pseudo-Boolean encodings. https://pysathq.github.io/
This solver can be used if the model only has Boolean variables, and only logical constraints (and,or,implies,==,!=) or cardinality constraints.
Documentation of the solver’s own Python API: https://pysathq.github.io/docs/html/api/solvers.html
WARNING: CPMpy uses ‘model’ to refer to a constraint specification, the PySAT docs use ‘model’ to refer to a solution.
List of classes
Interface to PySAT's API |
- class cpmpy.solvers.pysat.CPM_pysat(cpm_model=None, subsolver=None)[source]
Interface to PySAT’s API
Requires that the ‘python-sat’ python package is installed: $ pip install python-sat
See detailed installation instructions at: https://pysathq.github.io/installation.html
Creates the following attributes (see parent constructor for more): pysat_vpool: a pysat.formula.IDPool for the variable mapping pysat_solver: a pysat.solver.Solver() (default: glucose4)
The DirectConstraint, when used, calls a function on the pysat_solver object.
- get_core()[source]
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()
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
- objective(expr, minimize)
Post the given expression to the solver as objective to minimize/maximize
expr: Expression, the CPMpy expression that represents the objective function
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()
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, vals)[source]
PySAT supports warmstarting the solver with a feasible solution
In PySAT, this is called setting the ‘phases’ or the ‘polarities’ of literals
- Parameters
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
- solve(time_limit=None, assumptions=None)[source]
Call the PySAT solver
Arguments: - time_limit: maximum solve time in seconds (float, optional). Auto-interrups in case the
runtime exceeds given time_limit. Warning: the time_limit is not very accurate at subsecond level
- assumptions: list of CPMpy Boolean variables that are assumed to be true.
For use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together. Note: the PySAT interface is statefull, so you can incrementally call solve() with assumptions and it will reuse learned clauses
- solveAll(display=None, time_limit=None, solution_limit=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
- Arguments:
- 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
any other keyword argument
Returns: number of solutions found
- solver_var(cpm_var)[source]
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
- 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:
[bool]: Solver support by current system setup.
- transform(cpm_expr)[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.
- Parameters
cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof
- Returns
list of Expression