Formula processing (pysat.process
)#
List of classes#
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
- 1
Armin Biere, Matti Järvisalo, Benjamin Kiesl. Preprocessing in SAT Solving. In Handbook of Satisfiability - Second Edition. pp. 391-435
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 aCNF
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 thewith
statement, deletion is done automatically when the end of thewith
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()
andrestore()
. 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()
. AFalse
status indicates that the formula is found to be unsatisfiable by the preprocessor. Otherwise, the status equalsTrue
.- 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 astatus
variable, which is set toFalse
if the preprocessor found the original formula to be unsatisfiable (andTrue
otherwise). The same status value is set to thestatus
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
>>> 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]