Formula processing (`pysat.process`)#

List of classes#

Processor

This class provides interface to CaDiCaL's preprocessor.

Module description#

This module provides access to the preprocessor functionality of CaDiCaL 1.5.3. It can be used to process [1] (also see references therein) a given CNF formula and output a another formula, which is guaranteed to be equisatisfiable with the original formula. The processor can be invoked for a user-provided number of rounds. Also, the following preprocessing techniques can be used when running the processor:

blocked clause elimination
covered clause elimination
globally-blocked clause elimination
equivalent literal substitution
bounded variable elimination
failed literal probing
hyper binary resolution
clause subsumption
clause vivification

Note that the numerous parameters used in CaDiCaL for tweaking the preprocessor’s behavior are currently unavailable here. (Default values are used.)

>>> from pysat.formula import CNF
>>> from pysat.process import Processor
>>> from pysat.solvers import Solver
>>>
>>> cnf = CNF(from_clauses=[[1, 2], [3, 2], [-1, 4, -2], [3, -2], [3, 4]])
>>> processor = Processor(bootstrap_with=cnf)
>>>
>>> processed = processor.process()
>>> print(processed.clauses)
[]
>>> print(processed.status)
True
>>>
>>> with Solver(bootstrap_with=processed) as solver:
...     solver.solve()
True
...     print('proc model:', solver.get_model())
proc model: []
...     print('orig model:', processor.restore(solver.get_model()))
orig model: [1, -2, 3, -4]
>>>
>>> processor.delete()

Module details#

class pysat.process.Processor(bootstrap_with=None)#

This class provides interface to CaDiCaL’s preprocessor. The only input parameter is bootstrap_with, which is expected to be a CNF formula or a list (or iterable) of clauses.

Parameters:: bootstrap_with (CNF or iterable(iterable(int))) – a list of clauses for processor initialization.

Once created and used, a processor must be deleted with the delete() method. Alternatively, if created using the with statement, deletion is done automatically when the end of the with block is reached. It is important to keep the processor if a user wants to restore a model of the original formula.

The main methods of this class are process() and restore(). The former calls CaDiCaL’s preprocessor while the latter can be used to reconstruct a model of the original formula given a model for the processed formula as illustrated below.

Note how keeping the Processor object is needed for model restoration. (If it is deleted, the information needed for model reconstruction is lost.)

>>> from pysat.process import Processor
>>> from pysat.solvers import Solver
>>>
>>> processor = Processor(bootstrap_with=[[-1, 2], [1, -2]])
>>> processor.append_formula([[-2, 3], [1]])
>>> processor.add_clause([-3, 4])
>>>
>>> processed = processor.process()
>>> print(processed.clauses)
[]
>>> print(processed.status)
True
>>>
>>> with Solver(bootstrap_with=processed) as solver:
...     solver.solve()
True
...     print('proc model:', solver.get_model())
proc model: []
...     print('orig model:', processor.restore(solver.get_model()))
orig model: [1, 2, 3, 4]
>>>
>>> processor.delete()

add_clause(clause)#

Add a single clause to the processor.

Parameters:: clause (list(int) or any iterable(int)) – a clause to add

>>> processor = Processor()
>>> processor.add_clause([-1, 2, 3])

append_formula(formula)#

Add a given list of clauses into the solver.

Parameters:: formula (iterable(iterable(int)), or CNF) – a list of clauses.

>>> cnf = CNF()
... # assume the formula contains clauses
>>> processor = Processor()
>>> processor.append_formula(cnf)

delete()#: Actual destructor.

get_status()#

Preprocessor’s status as the result of the previous call to process(). A False status indicates that the formula is found to be unsatisfiable by the preprocessor. Otherwise, the status equals True.

Return type:: bool

process(rounds=1, block=False, cover=False, condition=False, decompose=True, elim=True, probe=True, probehbr=True, subsume=True, vivify=True)#

Runs CaDiCaL’s preprocessor for the internal formula for a given number of rounds and using the techniques specified in the arguments. Note that the default values of all the arguments used are set as in the default configuration of CaDiCaL 1.5.3.

As the result, the method returns a CNF object containing the processed formula. Additionally to the clauses, the formula contains a status variable, which is set to False if the preprocessor found the original formula to be unsatisfiable (and True otherwise). The same status value is set to the status variable of the processor itself.

It is important to note that activation of some of the preprocessing techniques conditionally depends on the activation of other preprocessing techniques. For instance, subsumed, blocked and covered clause elimination is invoked only if bounded variable elimination is active. Subsumption elimination in turn may trigger vivification and transitive reduction if the corresponding flags are set.

Parameters:

rounds (int) – number of preprocessing rounds
block (bool) – apply blocked clause elimination
cover (bool) – apply covered clause elimination
condition (bool) – detect conditional autarkies and apply globally-blocked clause elimination
decompose (bool) – detect strongly connected components (SCCs) in the binary implication graph (BIG) and apply equivalent literal substitution (ELS)
elim (bool) – apply bounded variable elimination
probe (bool) – apply failed literal probing
probehbr (bool) – learn hyper binary resolvents while probing
subsume (bool) – apply global forward clause subsumption
vivify (bool) – apply clause vivification

Returns:

processed formula

Return type:

CNF

>>> from pysat.process import Processor
>>>
>>> processor = Processor(bootstrap_with=[[-1, 2], [-2, 3], [-1, -3]])
>>> processor.add_clause([1])
>>>
>>> processed = processor.process()
>>> print(processed.clauses)
[[]]
>>> print(processed.status)
False  # this means the processor decided the formula to be unsatisfiable
>>>
>>> with Solver(bootstrap_with=processed) as solver:
...     solver.solve()
False
>>> processor.delete()

restore(model)#

Reconstruct a model for the original formula given a model for the processed formula. Done by using CaDiCaL’s extend() and reconstruction stack functionality.

Parameters:: model (iterable(int)) – a model for the preprocessed formula
Returns:: extended model satisfying the original formula
Return type:: list(int)

>>> from pysat.process import Processor
>>>
>>> with Processor(bootstrap_with=[[-1, 2], [-2, 3]]) as proc:
...     proc.add_clause([1])
...     processed = proc.process()
...     with Solver(bootstrap_with=processed) as solver:
...         solver.solve()
...         print('model:', proc.restore(solver.get_model()))
...
model: [1, 2, 3]

Pseudo-Boolean encodings (pysat.pb)

SAT solvers’ API (pysat.solvers)

Formula processing (pysat.process)#

List of classes#

Module description#

Module details#

Formula processing (`pysat.process`)#