Formula preprocessing (pyqbf.process)

List of classes

Bloqqer	Direct usage of the backend-interface of Bloqqer
Processor	API for compatibility with pysat.process.Processor

Module description

This module provides access to the Bloqqer-preprocessor. It implements the following techniques:

• Quantified Literal Elimination

• Quantified Blocked Clause Elimination

• Quantified Covered Blocked Clause Elimination

• Quantified Covered Tautology Elimination

• Subsumption

• Variable Expansion

• Equivalence Detection

Besides the class Bloqqer which is a direct implementation of the interface, there is also the class Processor implementing the exact same interface as pysat.process.Processor.

At the moment, no configuration is possible using the interface.

Module details

class pyqbf.process.Bloqqer

Direct usage of the backend-interface of Bloqqer

>>> from pyqbf.formula import PCNF
>>> from pyqbf.process import Processor
>>> from pyqbf.solvers import Solver
>>> 
>>> pcnf = PCNF(from_clauses=[[1, 2], [3, 2], [-1, 4, -2], [3, -2], [3, 4]], auto_generate_prefix=True)
>>> processor = Bloqqer()
>>> processed = processor.preprocess(pcnf)
>>> print(processed)
True        
>>> pcnf = PCNF(from_file="formula_not_being_solved_directly.qdimacs")
>>> processed = processor.preprocess(pcnf)
>>> type(processed)
<class 'pyqbf.formula.PCNF'>

preprocess(formula)

Processes the provided formula using Bloqqer

Parameters:

formula (pyqbf.formula.PCNF) – the target to preprocess

Returns:

True or False if the preprocessor was able to solve the formula. Else a formula describing the state after preprocessing

Return type:

bool or pyqbf.formula.PCNF

processor = Bloqqer()
processor.preprocess()

class pyqbf.process.Processor(bootstrap_with=None)

API for compatibility with pysat.process.Processor

Parameters:

bootstrap_with (pyqbf.formula.PCNF) – Formula to be preprocessed

>>> from pyqbf.formula import PCNF
>>> from pyqbf.process import Processor
>>> from pyqbf.solver import Solver
>>> 
>>> pcnf = PCNF(from_clauses=[[1, 2], [3, 2], [-1, 4, -2], [3, -2], [3, 4]], auto_generate_prefix=True)
>>> processor = Processor(bootstrap_with=pcnf)
>>> processed = processor.process()
>>> print(processed.clauses)
[]
>>> print(processor.status)
True

>>> with Solver(bootstrap_with=processed) as solver:
>>>     solver.solve()
True
...     print('proc model:', solver.get_model())
>>> proc model: []

add_clause(clause)

Add a single clause to the processor.

Parameters:

clause (list[int] or any iterable of type int) – a clause to add

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

append_formula(formula, no_return=True)

Add a given formula into the preprocessor.

For a list of clauses (list[list[int]]), they will be added to the clause-part of the internal pyqbf.formula.PCNF. For a (transformed) pyqbf.formula.PCNF, the non-occurring variables will be added at the end of the prefix existentially quantified.

Parameters:

• formula (e.g. pyqbf.formula.PCNF) – a list of clauses or another formula convertable to PCNF

• no_return (bool) – check processors’s internal formula and return the result, if set to False. Default True

Return type:

bool if no_return is set to False.

>>> pcnf = PCNF(from_file="formula.qdimacs")
>>> processor = Processor()
>>> processor.append_formula(pcnf)

get_status()

Preprocessor’s status as the result of the previous call to process(). If the preprocessor was not able to solve the formula or the function was not called yet, the status is None.

Returns:

The result of the last call of process()

Return type:

bool or None

>>> processor = Processor(bootstrap_with=[[-1, 2], [-2, 3], [-1, -3]])
>>> processed = processor.process()
>>> print(processor.get_status())
True

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

Run the preprocessor on the specified formula

Warning

All parameters are specified due to compatibility-reasons with pysat.process.Processor and will be ignored

>>> processor = Processor(bootstrap_with=[[-1, 2], [-2, 3], [-1, -3]])
>>> processor.add_clause([1])
>>> processed = processor.process()
>>> print(processed.clauses)
[[]]
>>> print(processor.status)
False

restore(model)

Compatibility method for pysat.process.Processor.

Warning

Not implemented for QBFs