External engines (`pysat.engines`)#

List of classes#

`Propagator`	An abstract class for creating external user-defined propagators / reasoning engines to be used with solver `Cadical195` through the IPASIR-UP interface.
`BooleanEngine`	A simple example Boolean constraint propagator inheriting from the class `Propagator`.
`LinearConstraint`	A possible implementation of linear constraints over Boolean variables, including cardinality and pseudo-Boolean constraints.
`ParityConstraint`	A possible implementation of parity constraints.

Module description#

This module provides a user with the possibility to define their own propagation engines, i.e. constraint propagators, attachable to a SAT solver. The implementation of this functionality builds on the use of the IPASIR-UP interface [1]. This may come in handy when it is beneficial to reason over non-clausal constraints, for example, in the settings of satisfiability modulo theories (SMT), constraint programming (CP) and lazy clause generation (LCG).

Note

Currently, the only SAT solver available in PySAT supporting the interface is CaDiCaL 1.9.5.

The interface allows a user to attach a single reasoning engine to the solver. This means that if one needs to support multiple kinds of constraints simultaneously, the implementation of the engine may need to be sophisticated enough to make it work.

It is imperative that any propagator a user defines must inherit the interface of the abstract class Propagator and defines all the required methods for the correct operation of the engine.

An example propagator is shown in the class BooleanEngine. It currently supports two kinds of example constraints: linear (cardinality and pseudo-Boolean) constraints and parity (exclusive OR, XOR) constraints. The engine can run in the adaptive mode, i.e. it can enable and disable itself on the fly.

Once an engine is implemented, it should be attached to a solver object by calling connect_propagator() of Cadical195. The propagator will then need to inform the solver what variable it requires to observe.

solver = Solver(name='cadical195', bootstrap_with=some_formula)

engine = MyPowerfulEngine(...)
solver.connect_propagator(engine)

# attached propagator wants to observe these variables
for var in range(some_variables):
    solver.observe(var)

...

Note

A user is encouraged to examine the source code of BooleanEngine in order to see how an external reasoning engine can be implemented and attached to CaDiCaL 1.9.5. Also consult the implementation of the corresponding methods of Cadical195.

Module details#

class pysat.engines.BooleanEngine(bootstrap_with=[], adaptive=True)#

A simple example Boolean constraint propagator inheriting from the class Propagator. The idea is to exemplify the use of external reasoning engines. The engine should be general enough to support various constraints over Boolean variables.

Note

Note that this is not meant to be a model implementation of an external engine. One can devise a more efficient implementation with the same functionality.

The initialiser of of the class object may be provided with a list of constraints, each being a tuple (‘type’, constraint), as a value for parameter bootstrap_with.

Currently, there are two types of constraints supported (to be specified) in the constraints passed in: 'linear' and 'parity' (exclusive OR). The former will be handled as objects of class LinearConstraint while the latter will be transformed into objects of ParityConstraint.

Here, each type of constraint is meant to have a list of literals stored in variable .lits. This is required to set up watched lists properly.

The second keyword argument adaptive (set to True by default) denotes the fact that the engine should check its own efficiency and disable or enable itself on the fly. This functionality is meant to exemplify how adaptive external engines can be created. A user is referred to the source code of the implementation for the details.

adaptive_constants(pdecay, pbound, mdecay, mbound)#: Set magic numeric constants used in adaptive mode.

adaptive_update(satisfied)#: Update adaptive mode: either enable or disable the engine. This depends on the statistics accumulated in the current run and whether or not the previous assignment found by the solver satisfied the constraints.

add_clause()#: Extract a new clause to add to the solver if one exists; return an empty clause [] otherwise.

add_constraint(constraint)#: Add a new constraint to the engine and integrate it to the internal structures, i.e. watched lists. Also, return the newly added constraint to the callee.

check_model(model)#: Check if a given model satisfies all the constraints.

cleanup_watched(lit, garbage)#: Garbage collect holes in the watched list for +lit (and potentially for -lit).

decide() → int#

This method allows the propagator to influence the decision process. Namely, it is used when the solver asks the propagator for the next decision literal (if any). If the method returns 0, the solver will make its own choice.

Return type:: int

disable()#: Notify the solver that the propagator should become inactive as it does not contribute much to the inference process. From now on, it will only be called to check complete models obtained by the solver (see check_model()).

enable()#: Notify the solver that the propagator is willing to become active from now on.

is_active()#: Return engine’s status. It is deemed active if the method returns True and passive otherwise.

on_assignment(lit, fixed)#: Update the propagator’s state given a new assignment.

on_backtrack(to)#: Cancel all the decisions up to a certain level.

on_new_level()#: Keep track of decision level updates.

preprocess()#: Run some (naive) preprocessing techniques if available for the types of constraints under considerations. Each type of constraints is handled separately of the rest of constraints.

process_linear()#

Process linear constraints. Here we apply simple pairwise summation of constraints. As the number of result constraints is quadratic, we stop the process as soon as we get 100 new constraints. Also, if a result of the sum is longer than each of the summands, the result constraint is ignored.

This is trivial procedure is made to illustrate how constraint processing can be done. It can be made dependent on user-specified parameters, e.g. the number of rounds or a numeric value indicating when a pair of constraints should be added and when they should not be added. For consideration in the future.

process_parity()#: Process parity/XOR constraints. Basically, this runs Gaussian elimination and see if anything can be derived from it.

propagate()#: Run the propagator given the current assignment.

provide_reason(lit)#: Return the reason clause for a given literal.

setup_observe(solver)#: Inform the solver about all the variables the engine is interested in. The solver will mark them as observed by the propagator.

class pysat.engines.LinearConstraint(lits=[], weights={}, bound=1)#

A possible implementation of linear constraints over Boolean variables, including cardinality and pseudo-Boolean constraints. Each such constraint is meant to be in the less-than form, i.e. a user should transform the literals, weights and the right-hand side of the constraint into this form before creating an object of LinearConstraint. The class is designed to work with BooleanEngine.

The implementation of linear constraint propagation builds on the use of counters. Basically, each time a literal is assigned to a positive value, it is assumed to contribute to the total weight on the left-hand side of the constraint, which is calculated and compared to the right-hand side.

The constructor receives three arguments: lits, weights, and bound. Argument lits represents a list of literals on the left-hand side of the constraint while argument weights contains either a list of their weights or a dictionary mapping literals to weights. Finally, argument bound is the right-hand side of the constraint.

Note that if no weights are provided, each occurrence of a literal is assumed to have weight 1.

Note

All weights are supposed to be non-negative values.

Parameters:

lits – list of literals (left-hand side)
weights (list or dict) – weights of the literals
bound (int or float) – right-hand side of the constraint

abandon_unweighted(dummy_lit)#: Clear the reason of a given literal.

abandon_weighted(lit)#: Clear the reason of a given literal.

attach_values(values)#: Give the constraint access to centralised values exposed from BooleanEngine.

explain_failure()#: Provide a reason clause for why the previous model falsified the constraint. This will clause will be added to the solver.

falsified_by(model)#: Check if the constraint is violated by a given assignment. Upon receiving such an input assignment, the method counts the sum of the weights of all satisfied literals and checks if it exceeds the right-hand side.

justify_unweighted(dummy_lit)#: Provide a reason for a literal propagated by this constraint. In the unweighted case, all the literals propagated by this constraint share the same reason.

justify_weighted(lit)#: Provide a reason for a literal propagated by this constraint. In the case of weighted constraints, a literal may have a reason different from the other literals propagated by the same constraint.

propagate_unweighted(lit=None)#: Get all the consequences of a given literal in the unweighted case. The implementation counts how many literals on the left-hand side are assigned to true.

propagate_weighted(lit=None)#: Get all the consequences of a given literal in the weighted case. The implementation counts the weights of all the literals assigned to true and propagates all the other literals (yet unassigned) such that adding their weights to the total sum would exceed the right-hand side of the constraint.

register_watched(to_watch)#: Add self to the centralised watched literals lists in BooleanEngine.

unassign(lit)#: Unassign a given literal, which is done by decrementing the literal’s contribution to the total sum of the weights of assigned literals.

class pysat.engines.Propagator#

An abstract class for creating external user-defined propagators / reasoning engines to be used with solver Cadical195 through the IPASIR-UP interface. All user-defined propagators should inherit the interface of this abstract class, i.e. all the below methods need to be properly defined. The interface is as follows:

class Propagator(object):
    def on_assignment(self, lit: int, fixed: bool = False) -> None:
        pass      # receive a new literal assigned by the solver

    def on_new_level(self) -> None:
        pass      # get notified about a new decision level

    def on_backtrack(self, to: int) -> None:
        pass      # process backtracking to a given level

    def check_model(self, model: List[int]) -> bool:
        pass      # check if a given assignment is indeed a model

    def decide(self) -> int:
        return 0  # make a decision and (if any) inform the solver

    def propagate(self) -> List[int]:
        return [] # propagate and return inferred literals (if any)

    def provide_reason(self, lit: int) -> List[int]:
        pass      # explain why a given literal was propagated

    def add_clause(self) -> List[int]:
        return [] # add an(y) external clause to the solver

add_clause() → List[int]#

The method is called by the solver to add an external clause if there is any. The clause can be arbitrary but if it is root-satisfied or tautological, the solver will ignore it without learning it.

Root-falsified literals are eagerly removed from the clause. Falsified clauses trigger conflict analysis, propagating clauses trigger propagation. Unit clauses always (unless root-satisfied, see above) trigger backtracking to level 0.

An empty clause (or root falsified clause, see above) makes the formula unsatisfiable and stops the search immediately.

Return type:: iterable(int)

check_model(model: List[int]) → bool#

The method is used for checking if a given (complete) truth assignment satisfies the constraint managed by the propagator. Receives a single argument storing the truth assignment found by the solver.

Note

If this method returns False, the propagator must be ready to provide an external clause in the following callback.

Parameters:: model (iterable(int)) – a list of integers representing the current model
Return type:: bool

decide() → int#

Return type:: int

on_assignment(lit: int, fixed: bool = False) → None#

The method is called to notify the propagator about an assignment made for one of the observed variables. An assignment is set to be “fixed” if it is permanent, i.e. the propagator is not allowed to undo it.

Parameters:

lit (int) – assigned literal
fixed (bool) – a flag to mark the assignment as “fixed”

on_backtrack(to: int) → None#

The method for notifying the propagator about backtracking to a given decision level. Accepts a single argument to signifying the backtrack level.

Parameters:: to (int) – backtrack level

on_new_level() → None#: The method called to notify the propagator about a new decision level created by the solver.

propagate() → List[int]#

The method should invoke propagation under the current assignment. It can return either a list of literals propagated or an empty list [], informing the solver that no propagation is made under the current assignment.

Return type:: int

provide_reason(lit: int) → List[int]#

The method is called by the solver when asking the propagator for the reason / antecedent clause for a literal the propagator previously inferred. This clause will be used in the following conflict analysis.

Note

The clause must contain the propagated literal.

Parameters:: lit (int) – literal to provide reason for
Return type:: iterable(int)

Boolean formula manipulation (pysat.formula)

Pseudo-Boolean encodings (pysat.pb)

External engines (pysat.engines)#

List of classes#

Module description#

Module details#

External engines (`pysat.engines`)#