Solver Module

This module for solving task instances of some Problem that arise when substituting specific values of Variables that are presented in the Encoding.

Solver

Module interface for defining the Problem solving tool. It has one inherited method: get_instance(…), which should return an instance of _Solver.

class lib_satprob.solver.Solver()

Base Solver class constructor haven’t any arguments.

Report

A structure for representing the solver’s output and associated statistics.

class lib_satprob.solver.Report(
    status: Optional[bool]
    stats: Dict[str, float]
    model: List[int]
    cost: int
)

KeyLimit

An tuple to limit the solver’s process resources for one run.

type lib_satprob.solver.KeyLimit = Tuple[str, float]

Example:

time_limit = ('time', 5) # 5 seconds
conflicts_limit = ('conflicts', 1000) # 1000 conflicts
propagations_limit = ('propagations', 1000) # 1000 propagations

Solver Methods

get_instance(formula, use_timer)

This method creates an instance of solver for given formula. Created solver instance allows to propagate or solve a given formula multiple times on different Supplements without reinitialising the wrapped solver.

Note

Currently, reinitialising is skipped only if the formula is a pysat.formula.CNF instance (that is, the encoding is CNF or CNFPlus instance) instance and the passed supplements contains only an Assumptions part.

Input arguments:

formula (Formula) - a encoding formula returned by Encoding.get_formula(…) method.
use_timer (Optional[boolean]) - a flag to enable timer while solving. If timer disabled then resulting Report doesn’t contain time value in stats dictionary. Default: True.

Return type: _Solver

propagate(formula, supplements, use_timer)

This method makes propagation for given formula. First, all Constraints from the passed supplements are substituted into the formula, then the pysat.solvers.Solver.propagate(…) method is called with the list of Assumptions from the passed supplements.

Note

The method Solver.propagate(…) works only for CNF or CNFPlus encodings (that is, for SAT problems specified by the implementation of SatProblem).

Input arguments:

formula (Formula) - a encoding formula returned by Encoding.get_formula(…) method.
supplements (Supplements) - a formula supplements that are added while formula solving or propagating.
use_timer (Optional[boolean]) - a flag to enable timer while solving. If timer disabled then resulting Report doesn’t contain time value in stats dictionary. Default: True.

Return type: Report

solve(formula, supplements, limit, extract_model, use_timer)

This method solves given formula. First, Constraints from the passed supplements are substituted into the formula, then the pysat.solvers.Solver.solve(…) method is called with the list of Assumptions from the passed supplements and resource limit. The extract_model argument determines whether the satisfying assignment for the formula will be extracted from pysat solver.

Input arguments:

formula (Formula) - a encoding formula returned by Encoding.get_formula(…) method.
supplements (Supplements) - a formula supplements that are added while formula solving or propagating.
limit (Optional[KeyLimit]) - a solving limit. Default: (None, 0).
extract_model (Optional[boolean]) - a flag to extract a satisfying assignment for the formula given to the solver. Default: True.
use_timer (Optional[boolean]) - a flag to enable timer while solving. If timer disabled then resulting Report doesn’t contain time value in stats dictionary. Default: True.

Return type: Report

PySatSolver

Implementation for pysat solver. … about lib

class lib_satprob.solver.PySatSolver(sat_name='m22': str, max_sat_alg='rc2': str)

Init arguments:

sat_name (Optional[str]) - argument specifies …
max_sat_alg (Optional[str]) - argument specifies …

This implementation может использоваться для решения SAT and MaxSAT проблем.