Solver Model

_Solver

Base interface for incremental solver instance with predefined formula and use_timer parameter.

Note

To create an instance of this class use method get_instance(…).

propagate(supplements)

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.

Input arguments:

supplements (Supplements) - a formula supplements that are added while formula solving or propagating.

solve(supplements, limit, extract_model)

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:

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.