QBF solver’s API (`pyqbf.solvers`)#

List of classes#

`Solver`	High-Level API for compatibility with `pysat.Solver`
`Caqe`	Interface class for the usage of the Caqe-solver.
`DepQBF`	Interface class for the DepQBF-Solver
`QFun`	Interface class for the QFun-Solver
`QuAPI`	Base class for usage of the QuAPI-Interface for assumptions with non-assuming solvers.
`Qute`	Interface for the Qute-Solver
`RAReQS`	Interface class for the RAReQS-Solver
`SolverNames`	Contains all available solvers that can be instantiated by the `Solver`-class
`pyqbf_incremental_solver`	Base class for all solvers with incremental abilities
`pyqbf_solver`	Base class for all solvers of the pyqbf module
`AssumingEnvironment`	An simple, high-level API for solving with assumptions

List of methods#

`any_incremental_solver`	Provides a pre-configured solver for incremental solving.
`solve`	Providing the most basic functionality one would expect: solving the given formula.
`solve_all_files`	Loads the formulas from a given list of targets and solves them.
`solve_file`	Loads the formula from a given target and solves it.

List of constants#

DISABLE_WARNING_NON_ASSUMING

If set to true, this variable will supress warnings about using assumptions with a non-assuming solver

Module description#

This module provides access to a few modern QBF solvers. Currently supported are

Additionally, for making assumptions with non-assuming solvers, the QuAPI interface can be used by providing a path to a solver-executable.

The Backend-API of the solver is exposed in the classes having the same name as the solvers (DepQBF, QFun, Qute, RAReQS, Caqe, QuAPI) In contrast to the pysat.solvers-module there is no necessity to use a with-block or manual delete(), as weakref will take care of the cleanup when the objects run out of scope.

Similar to the pysat.solvers.Solver-class, the Solver will provide a higher API-level for those solvers.

Note

All functions from pysat.solvers.Solver are also availabe in the QBF-counterpart, but not every functionality is implement

Thus, a solver can be used the following ways:

>>> s = DepQBF()
>>>
>>> s = Solver(name='depqbf')

Note

We still recommend using the with-block when working with solvers as this causes the object to go out of scope faster and allows cleanup. All solvers will support being used in such a way.

As for its CNF-counterpart, the pyqbf.solvers module is designed to provide QBF solvers as oracles without exposing internal states. The following functionalities are currently supported

creating and deleting solver objects
adding clauses and formulas to the solvers
use different configurations-values
checking satisfiability with and without assumptions
extracting a (partial) model from a satisfiable formula
enumerating models of an input formula

PyQBF supports non-incremental and incremental solving, where QuAPI is used for allowing non-assuming solvers to make assumptions and solve incrementally.

For those who just need a fast interface for QBF utilities, we provide the very basic use-cases in form of pre-configuration.

Function solve() for fast oracle-calls without instantiation of a solver
Function solve_file() and solve_all_files() for fast oracle-calls for QDIMACS-file(s)
Function any_incremental_solver() for providing a preconfigured Solver-object fit for incremental solving
Class AssumingEnvironment for incremental solving with assumptions

>>> pcnf = ...
>>> solve(pcnf)
True
>>> solve_file("my_formula.qdimacs")
False
>>> solve_all_files(["f1.qdimacs", "f2.qdimacs"])
{"f1.qdimacs": True, "f2.qdimacs": False}
>>> with any_incremental_solver(bootstrap_with=pcnf) as solver:
...     solver.solve()
...     solver.add_clause([1, 2, 3])
...     solver.solve(assumptions=[3, 4])                
>>> with AssumingEnvironment(pcnf) as solver:
>>>     solver.solve([1, 2, 3])
>>>     solver.solve([1, -2, -3])
>>>     solver.solve([-1, -2, 3])

Module details#

class pyqbf.solvers.AssumingEnvironment(formula)#

Bases: object

An simple, high-level API for solving with assumptions

Parameters:: formula (pyqbf.formula.PCNF) – the target-formula to be solved with assumptions

Usage example:

>>> formula = PCNF(from_file="formula.qdimacs", auto_generate_prefix=True) 
>>> with AssumingEnvironment(formula) as solver:
...     print(solver.solve())                   #solve without assumptions
...     print(solver.solve([-1, 2, 3, 4, 5]))   #solve with specified assumptions
...     print(solver.solve([1, 2, -3]))         #solve with specified assumptions
True
False
True

solve(assumptions=[])#

Solves the formula with the provided assumptions. If no assumptions are provided, the original formula is solved

Parameters:: assumptions (list[int]) – a list of assumptions
Returns:: True, if the formula is satisfiable under these assumptions
Return type:: bool

Usage example:

>>> formula = PCNF(from_file="formula.qdimacs", auto_generate_prefix=True) 
>>> with AssumingEnvironment(formula) as solver:
...     print(solver.solve())                   #solve without assumptions
...     print(solver.solve([-1, 2, 3, 4, 5]))   #solve with specified assumptions
...     print(solver.solve([1, 2, -3]))         #solve with specified assumptions
True
False
True

class pyqbf.solvers.Caqe#

Bases: QuAPI

Interface class for the usage of the Caqe-solver. As the original source code is Rust, the integration is done by using the executable with the QuAPI-Interface

class Configuration(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#

Bases: Enum

Enum providing a variety of configuration option for the Caqe-solver

configure(option)#

Allows the configuration of the solver using either a string or the Caqe.Configuration-Enum

Parameters:: option (Caqe.Configuration or str) – the option to configure

Usage example:

>>> s = Caqe()
>>> s.configure(Caqe.Configuration.no_abstraction_equivalence)
>>> s.configure("--expansion_refinement=light")

pyqbf.solvers.DISABLE_WARNING_NON_ASSUMING = False#: If set to true, this variable will supress warnings about using assumptions with a non-assuming solver

class pyqbf.solvers.DepQBF(dynamic_nenofex=False, incr=False)#

Bases: pyqbf_incremental_solver

Interface class for the DepQBF-Solver

class Configuration(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#

Bases: Enum

Enum providing a variety of configuration option for the DepQBF-solver

configure(option)#

Allows the configuration of the solver using either a string or the DepQBF.Configuration-Enum

Parameters:: option (DepQBF.Configuration or str) – the option to configure

Usage example:

>>> s = DepQBF()
>>> s.configure(DepQBF.Configuration.qdo)
>>> s.configure(DepQBF.Configuration.max_dec(100))
>>> s.configure("--lclauses-init-size=4")

class pyqbf.solvers.QFun#

Bases: pyqbf_solver

Interface class for the QFun-Solver

solve(formula)#

Interface method for solving a PCNF-formula with the solver

Parameters:: formula (pyqbf.formula.PCNF) – a formula to be solved
Returns:: True, if the formula is SAT, else False
Return type:: bool

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> solver = QFun()
>>> print(solver.solve(pcnf))
True            

class pyqbf.solvers.QuAPI(solver_path, solver_id=None)#

Bases: pyqbf_solver

Base class for usage of the QuAPI-Interface for assumptions with non-assuming solvers. It can either be initialized with an executable-path or by using the preset by specifying the solver-id

Parameters:

solver_path (str) – path to the executable QuAPI should be used with
solver_id (int) – if specified, a the preset of the solver with this id is used as executable

Note

Using a preset should be done via the use_quapi-parameter of the Solver class rather than by instantiating this class directly.

The object can be used the following: if you want to solve a formula pcnf:

>>> solver = QuAPI("/path/to/solver")
>>> print(solver.solve(pcnf))
True

For configuration or assuming calls, the internal solver has to be bootstrapped with the formula. Thus create_internal_solver() has to be called once configuration is finished

>>> solver = QuAPI("/path/to/solver")
>>> solver.configure("conf1")
>>> solver.configure("conf2")
>>> ...
>>> solver.create_internal_solver(max_assumptions=5, formula=pcnf)
>>> #Now you can assume and solve as much as you want

A more advanced example:

>>> solver = QuAPI("/path/to/solver")
>>> solver.configure("--solverargument")
>>> solver.create_internal_solver(max_assumptions=5, formula=pcnf)
>>> solver.assume([1, 2])
>>> print(solver.solve())
True
>>> solver.assume([4, 5])
>>> print(solver.solve())
False

In order to use QuAPI safely, there are some things that have to be considered. For example, assumptions should only be done on variables with id less or equal than max_assumptions. Otherwise, if the assumed variable is universial, this is trivially false. Also, QuAPI might change quantifiers of the formula during initialization, making an unsound result possible if used incorrectly.

PyQBF already does some usability-checks in order to avoid misleading results. If you know what you are doing and actually want to use QuAPI this way, you can deactivate this checks by calling allow_unsafe(). Here is an example:

>>> pcnf = PCNF(from_clauses=[[-4, 1, 2, 3], [-5, -1], [4, 5]])
>>> pcnf.exists(1, 2).forall(3).exists(4, 5)
>>> # We know that 4 and 5 are Tseitin variables simplified with Plaisted-Greenbaum
>>> solver = QuAPI("/path/to/solver")
>>> solver.create_internal_solver(max_assumptions=2)
>>> solver.assume([-4])
Traceback (most recent call last):
...
RuntimeError: Trying to assume variable 4, which is out of range for max-assumption count of 2!
>>> solver.allow_unsafe()
>>> solver.assume([-4])
>>> solver.assume([-5])
>>> print(solver.solve())
False

allow_unsafe()#

When calling this method, all usability-checks will be disabled.

Warning

It is advised to only do this, when you know what you are doing. This may allow the formula to be changed by QuAPI in an unsound way if used incorrectly!

Returns:: The current QuAPI-class for chaining
Return type:: QuAPI

assume(clause_or_lit)#

Adds an assumption to the solver. This is only possible if the solver is already instantiated

Parameters:: clause_or_lit (int or list[int]) – the literal or list of literals containing the assumption(s)

Usage example:

>>> solver = QuAPI("/path/to/solver")
>>> formula = PCNF(from_file="some-formula.qdimacs")
>>> solver.create_internal_solver(5, formula)
>>> solver.assume([1, -2, 3, -4, 5])
>>> print(solver.solve())
False
>>> print(solver.solve([1, 2]))
True

property assuming#

Indicates whether the solver supports assumptions

Usage example:

>>> s = Qute()
>>> print(s.assuming)
False
>>> s = DepQBF()
>>> print(s.assuming)
True

configure(option)#

Configures the solver with the specified option

Parameters:: option (str) – configuration-string to be applied

create_internal_solver(max_assumptions, formula, allow_missing_universal_assumptions=False)#

Instantiates the internal solver with the configuration set so far

Parameters:

max_assumptions (int) – maximal count of assumptions allowed
formula (PCNF) – The formula to instantiate the solver with
allow_missing_universal_assumptions (bool) – if set to true, QuAPI will not terminate if universal assumptions are missing.

solve(formula=None, max_assumptions=0)#

Interface function for the QuAPI solving

Parameters:

formula (pyqbf.formula.PCNF) – the formula to be solve. Only necessary if the solver was not already instantiated
max_assumptions (int) – the maximal amount of assumptions. Only necessary if the solver was not already instantiated and assumptions should be added

Returns:

True, if the formula is satisfiable

Return type:

bool

Usage example:

>>> solver = QuAPI("/path/to/solver")
>>> formula = PCNF(from_file="some-formula.qdimacs")
>>> solver.create_internal_solver(5, formula)
>>> print(solver.solve())
True
>>> solver = QuAPI("/path/to/solver2")
>>> print(solver.solve(formula))
True
>>> solver = QuAPI("/path/to/solver3")
>>> print(solver.solve(formula, max_assumptions=2))
True
>>> solver.assume([1, -2])
>>> print(solver.solve())
False

class pyqbf.solvers.Qute#

Bases: pyqbf_solver

Interface for the Qute-Solver

class Configuration(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#

Bases: Enum

Enum providing a variety of configuration option for the Qute-solver

configure(option)#

Allows the configuration of the solver using either a string or the Qute.Configuration-Enum

Parameters:: option (Qute.Configuration or str) – the option to configure

Usage example:

>>> s = Qute()
>>> s.configure(Qute.Configuration.no_phase_saving)
>>> s.configure(Qute.Configuration.var_activity_inc(4))
>>> s.configure("--restarts=EMA")

Note

Not all configuration options of the Qute-Solver are available at the moment. A RuntimeError will be raised if such an option is specified.

solve(formula)#

Interface method for solving a PCNF-formula with the solver

Parameters:: formula (pyqbf.formula.PCNF) – a formula to be solved
Returns:: True, if the formula is SAT, else False
Return type:: bool

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> solver = QFun()
>>> print(solver.solve(pcnf))
True            

class pyqbf.solvers.RAReQS#

Bases: pyqbf_solver

Interface class for the RAReQS-Solver

class pyqbf.solvers.Solver(name='depqbf', bootstrap_with=None, use_timer=False, incr=False, **kwargs)#

Bases: object

High-Level API for compatibility with pysat.Solver

Raises:

ReferenceError – if there is no solver matching the given name
TypeError – if one of the arguments in kwargs is not valid

Parameters:

name (str or SolverNames) – The name or :class:SolverNames-enum of the solver to choose. Default "depqbf"
bootstrap_with (pyqbf.formula.PCNF or anything a PCNF can be constructed from with the pyqbf.formula.to_pcnf-method) – The formula the solver should be initialized. if None, an empty PCNF is created. Default None
use_timer (bool) – If true, the solver will measure how long the solving takes. Default False
incr (bool) – If true, the solver will be configured to allow incremental solving if possible. Default False

Allowed kwargs:

Parameters:

use_quapi (bool) – If true, the QuAPI will be used for the solver
quapi_custom_path (str) – Path to an executable for a custom QuAPI solver
quapi_max_assumption_size (int) – The maximal number of assumptions in a run. Has to be set when using quapi. Default will be the size of the prefix
quapi_solver_configurations (list[str]) – An array of additional configuration-strings passed to the solver-backend of QuAPI
quapi_allow_missing_universials (bool) – Indicates whether the usage of missing universial assumptions is permitted

Usage example:

>>> s = Solver()
>>> s.add_clause([1, 2])
>>> s.add_clause([-1, -2])
>>> s.formula.forall(1).exists(2)
>>> print(s.solve())
True
>>> print(s.get_model()) #no model as first block is universially quantified
[]
>>>
>>> f = PCNF(from_file="some-file.qdimacs")
>>> s = Solver(name=SolverNames.qfun, bootstrap_with=f)
>>> print(s.solve())
False
>>>
>>> s = Solver(quapi_custom_path="/path/to/depqbf", use_quapi=True, quapi_max_assumption_size=5,
...            bootstrap_with=f, quapi_solver_configurations=[DepQBF.Configuration.qdo])
>>>print(s.solve())
False
>>>
>>> s = Solver(name=SolverNames.depqbf, use_quapi=True, bootstrap_with=f)
...    s.assume([1, 2])
>>> print(s.solve())
False
>>>
>>> with Solver(name=SolverNames.depqbf, incr=True) as solver:
...     solver.append_formula(PCNF(from_file="some-other-file.qdimacs"))
...     print(solver.solve())
...     solver.add_clause([1, 2, 3])
...     print(solver.solve())
...
True
False

accum_stats()#

Get accumulated low-level stats from the solver. Currently, the statistics includes the number of restarts, conflicts, decisions, and propagations

Returns:: a dictionary containing the accumulated stats
Return type:: dict

Usage example:

>>> formula = PCNF(from_file="some-file.qdimacs")
>>> with Solver(name=SolverNames.depqbf,bootstrap_with=formula) as solver:
...    solver.solve()
...    print(solver.accum_stats()) #note that depqbf does not provide conflicts
...
{'restarts': 2, 'conflicts': 0, 'decisions': 254, 'propagations': 2321}

add_atmost(lits, k, no_return=True)#

Warning

This function is not supported by QBFs!

Raises:: NotImplementedError

add_clause(clause, no_return=True)#

Adds a single clause to the solver. The optional argument no_return controls whether or not to check the formula’s satisfiability after adding the new clause.

Parameters:

clause (iterable(int)) – an iterable over literals.
no_return (bool) – check solver’s internal formula and return the result, if set to False.

Return type:

bool if no_return is set to False.

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> solver = Solver(bootstrap_with=pcnf)
>>> solver.add_clause([-1, 2])
>>> solver.add_clause([-3, 4], no_return=False)
True

add_xor_clause(lits, value=True)#

Warning

This function is not supported by QBFs!

Raises:: NotImplementedError

append_formula(formula, no_return=True)#

This method can be used to add a given formula into the solver.

For a list of clauses, this will be added to the clause-part of the internal PCNF. For a PCNF or object transformed from a PCNF, the non-occurring variables will be added at the end of the prefix

Parameters:

formula (e.g. pyqbf.formula.PCNF) – a list of clauses or another formula convertable to pyqbf.formula.PCNF
no_return (bool) – check solver’s internal formula and return the result, if set to False. Default True

Return type:

bool if no_return is set to False

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> s = Solver()
>>> s.append_formula(pcnf)
>>> s.solve()
True
>>>
>>> s = Solver()
>>> s.append_formula(pcnf, no_return=False)
True

assume(clause_or_lit)#

Adds an assumption to the next solver-run. Only available with incremental solvers or QuAPI.

Parameters:: clause_or_lit (int or list[int]) – a clause of assumptions or a single assumption to be added to the solver
Raises:: RuntimeError, if the solver does not support assumptions

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> with Solver(name=SolverNames.depqbf, bootstrap_with=pcnf) as solver:
...     solver.assume([1, 2])
...     solver.assume(3)
...     print(solver.solve())
...
True

clear_interrupt()#

Warning

This function is currently unsupported

Raises:: NotImplementedError

conf_budget(budget=-1)#

Set limit on the number of conflicts.

Parameters:: budget (int) – the upper bound on the number of conflicts
Raises:: NotImplementedError, if the solver does not support limitation of conflicts

Warning

Currently not supported by our framework

configure(*options)#

Set further configuration values of the chosen solver. For the available options, use the <Solver-Class>.Configuration enum to set the configuration values

Parameters:: options (str or enum.Enum) – a vararg-list of configurations (either an element of one of the Configuration-enums or str)

Usage example:

>>> s = Solver(name=SolverNames.depqbf)
>>> s.configure(DepQBF.Configuration.qbo)
>>>
>>> s = Solver(name=SolverNames.qute)
>>> s.configure(Qute.Configuration.no_phase_saving)
>>>
>>> s = Solver(quapi_custom_path="/path/to/solver", use_quapi=True)
>>> s.configure("--custom-flag")

dec_budget(budget)#

Set limit on the number of decisions.

Parameters:: budget (int) – the upper bound on the number of decisions
Raises:: NotImplementedError, if the solver does not support limitation of decisions

Note

In contrast to pysat.solvers.Solver.dec_budget(), this is equivalent to setting a configuration value

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> s = Solver(name=SolverNames.depqbf, bootstrap_with=pcnf)
>>> s.dec_budget(500)
>>> s.solve()
False

delete()#: Manual destruction of the solver. Can be used for clean-up.

Note

This is not necessary if used in a with-block. In general, cleanup is also automatically done after the solver-variable goes out of scope.

enum_models(assumptions=[])#

Enumerates the models of the outermost existential quantifier block.

Note

This function is only supported if the solver-backend supports and is configured for incremental solving!

Usage example:

>>> pcnf = PCNF(from_clauses=[[-1, 2, 3], [1, -2, -3]])
>>> pcnf.exists(1, 2).forall(3)
>>> with Solver(incr=True, bootstrap_with=pcnf) as solver:
...     print(list(solver.enum_models))
[[1, 2], [-1, -2]]

get_core()#

Extract the unsatisfiable core of the formula

Raises:: NotImplementedError

Warning

This is currently not supported

get_model()#

Retrieves the model of the outermost existential quantifier block

Return type:: list[int]

Usage example:

>>> pcnf = PCNF(from_clauses=[[-1, 2, 3], [1, -2, -3]])
>>> pcnf.exists(1, 2).forall(3)
>>> with Solver(bootstrap_with=pcnf) as solver:
...     solver.solve()
...     print(solver.get_model())
...
[-1, -2]

get_proof()#

Returns a proof certificate

Raises:: NotImplementedError

Warning

At the moment, no included solver supports the QRAT format

Raises:: NotImplementedError

get_status()#

Obtains the result of the previous SAT call.

Return type:: bool or None.

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> solver = Solver(bootstrap_with=pcnf):
>>> print(solver.solve())
True
>>> print(solver.get_status())
True

interrupt()#

Warning

This function is currently unsupported

Raises:: NotImplementedError

nof_clauses()#

Returns the number of clauses currently occurring in the formula

Return type:: int

Usage example:

>>> s = Solver(bootstrap_with=[[-1, 2], [1, -2], [1, 2]])
>>> s.nof_clauses()
3

nof_vars()#

Returns the number of quantified variables currently occurring in the prefix

Return type:: int

process(**kwargs)#

Preprocesses the formula. This is done by Bloqqer using the pyqbf.process-module

Returns:: The result if the formula was solved. Else None - in this case the internal formula is the formula retrieved from the preprocessor
Return type:: bool or None

Usage example:

>>> pcnf = PCNF(from_clauses=[[-1, 2], [1, -2]])
>>> pcnf.forall(1).exists(2)
>>> s = Solver(bootstrap_with=pcnf)
>>> print(s.process())
True
>>> pcnf = PCNF(from_file="formula_not_being_solved_directly.qdimacs")
>>> s = Solver(bootstrap_with=pcnf)
>>> print(s.process())
None
>>> print(s.formula)
<Preprocessed formula>

prop_budget(budget)#

Set limit on the number of propagations.

Parameters:: budget (int) – the upper bound on the number of propagatoins
Raises:: NotImplementedError, if the solver does not support limitation of propagations

Warning

Currently not supported by our framework

propagate(assumptions=[], phase_saving=0)#

Warning

This function is currently unsupported

Raises:: NotImplementedError

set_phases(literals=[])#

Warning

This function is currently unsupported

Raises:: NotImplementedError

solve(assumptions=[])#

This method is used to check satisfiability of the internal formula

Parameters:: assumptions (list[int]) – A list of literals to be assumed for this run

Note

If the solver does not support assumptions, it will add unit-clauses directly to the formula. In this case a warning will be printed, which can be disabled by setting DISABLE_WARNING_NON_ASSUMING to True

Return type:: bool or None

Usage example:

>>> formula = PCNF(from_file="some-file.qdimacs")
>>> s = Solver(bootstrap_with=formula)
>>> s.solve()
True
>>> s.solve([1, 2])
False

solve_limited(assumptions=[], expect_interrupt=False)#

Warning

This function is currently unsupported

Raises:: NotImplementedError

start_mode(warm=False)#

Warning

Warm-starts are not supported by QBFs

Raises:: NotImplementedError

supports_assumptions()#

Indicates whether the solver supports assumptions

Returns:: True if assumptions are supported
Return type:: bool

supports_atmost()#

Note

Currently, no implemented solver supports atmost-encodings

Returns:: False
Return type:: bool

supports_incremental()#

Indicates whether the solver supports incremental solving

Returns:: True if incremental solving is supported
Return type:: bool

class pyqbf.solvers.SolverNames(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#

Bases: Enum

Contains all available solvers that can be instantiated by the Solver-class

pyqbf.solvers.any_incremental_solver(bootstrap_with=None)#

Provides a pre-configured solver for incremental solving. If the only goal is getting an incremental solver without thinking about which solver or configuration, this function may be used.

Parameters:: bootstrap_with – The formula to be solved. If none is provided, an empty formula is used.
Returns:: The preconfigured solver
Return type:: Solver

Usage example:

>>> formula = PCNF(from_file="some-file.qdimacs")
>>> solver = any_incremental_solver(formula)
>>> print(solver.solve())
True
>>> solver.add_clause([-1,2])
>>> print(solver.solve())
True
>>> solver.append_formula(PCNF(from_clauses=[[1,-2]]))
>>> print(solver.solve())
False

class pyqbf.solvers.pyqbf_incremental_solver(sid)#

Bases: pyqbf_solver

Base class for all solvers with incremental abilities

Parameters:: sid (int) – solver-id for the backend

add(clause)#

Interface method for adding a clause to the current frame of the incremental solver. Note: Resetting the solver after calling add after solving is done automatically

Parameters:: clause (list[int]) – a list of literals to be added to the solver

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]], auto_generate_prefix=True)
>>> solver = DepQBF()
>>> solver.load(pcnf)
>>> solver.add([-1, 2])            

add_var(var)#

Interface method for adding a variable to the current frame of the incremental solver. Note: Resetting the solver after calling add_var after solving is done automatically

Parameters:: var (int) – variable to be added

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]], auto_generate_prefix=True)
>>> solver = DepQBF()
>>> solver.load(pcnf)
>>> solver.add_var(3)

assume(clause_or_lit)#

Interface method for assuming the value of a variable

Parameters:: clause_or_lit (int or list[int]) – a clause of assumptions or a single assumption to be added to the solver
Raises:: TypeError if the provided parameter is neither int or list[int]

Usage example:

>>> solver = DepQBF()
>>> sut = PCNF(from_clauses=[[1,2], [1,-2]])
>>> sut.exists(1).forall(2)
>>> solver.assume(-1)
>>> print(solver.solve(sut))
False
>>> print(solver.solve())   # assumptions are resetted with the next call of solve()
True

property assuming#

Indicates whether the solver supports assumptions

Usage example:

>>> s = Qute()
>>> print(s.assuming)
False
>>> s = DepQBF()
>>> print(s.assuming)
True

load(formula)#

Interface method for loading a formula into the solver. This method may only be called once for loading the formula into the solver. For incremental solving the add()-function may be used

Parameters:: formula (pyqbf.formula.PCNF) – a PCNF formula
Raises:: RuntimeError if there already was a formula loaded into the solver.

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]], auto_generate_prefix=True)
>>> solver = DepQBF()
>>> solver.load(pcnf)
>>> solver.solve()
True
>>> # Equivalent to
>>> solver = DepQBF()
>>> solver.solve(pcnf)

pop()#

Interface method for popping the current frame. All clauses added after calling this function are added to the previous frame.

Usage example:

>>> solver = DepQBF()
>>> sut = PCNF(from_clauses=[[1,2]])        
>>> sut.exists(1,2)       
>>> print(solver.solve(sut))
True
>>> solver.push()   # new frame
>>> solver.add([-1,2])
>>> solver.add([1,-2])
>>> solver.add([-1,-2])
>>> print(solver.solve())
False
>>> solver.pop()   # remove last frame
>>> print(solver.solve())        
True

push()#

Interface method for pushing a new frame. All clauses added after calling this function are added to the new frame.

Usage example:

>>> solver = DepQBF()
>>> sut = PCNF(from_clauses=[[1,2]])        
>>> sut.exists(1,2)       
>>> print(solver.solve(sut))
True
>>> solver.push()   # new frame
>>> solver.add([-1,2])
>>> solver.push()   # new frame
>>> solver.add([1,-2])
>>> solver.push()   # new frame
>>> solver.add([-1, -2])
>>> print(solver.solve())
False

reset()#

Resets the internal solver states, keeps prefix and clauses. A reset is necessary after calls of the solve()-function.

Note

Resets are normally done automatically by the solver, such that this function rarely has to be called explicitely

>>> solver = DepQBF()
>>> sut = PCNF(from_clauses=[[1,2], [1,-2]])
>>> sut.exists(1).forall(2)
>>> solver.assume(-1)
>>> print(solver.solve(sut))
False
>>> solver.reset()    #would be done automatically
>>> print(solver.solve())
True

solve(formula=None)#

Interface method for solving a PCNF-formula with the incremental solver

Parameters:: formula (pyqbf.formula.PCNF) – a PCNF-formula to be solved. Note that this may only be specified once per solver, as incremental solving does not support the loading of multiple formulas
Returns:: True, if the formula is SAT, else False
Return type:: bool

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]], auto_generate_prefix=True)
>>> solver = DepQBF()
>>> print(solver.solve(pcnf))
True
>>> solver.add([-1, 2]) 
>>> print(solver.solve())
True
>>> solver.assume([1, 2])
>>> print(solver.solve())
False

class pyqbf.solvers.pyqbf_solver(sid)#

Bases: ABC

Base class for all solvers of the pyqbf module

Parameters:: sid (int) – solver-id for the backend

property alive#

Indicates if the finalizer of the object is active. This should always be True.

Usage example:

>>> s = QFun()
>>> print(s.alive)
True

property assuming#

Indicates whether the solver supports assumptions

Usage example:

>>> s = Qute()
>>> print(s.assuming)
False
>>> s = DepQBF()
>>> print(s.assuming)
True

configure(option)#

Configures the solver with the specified option

Parameters:: option (str) – configuration-string to be applied

get_assignment(var)#

Interface method for retrieving the assignment value of the specified variable

Parameters:: var (int) – variable to retrieve the assignment for
Returns:: The assignment of the specified variable if a model was previously computed
Return type:: int

get_stats()#

Get accumulated low-level stats from the solver. Currently, the statistics includes the number of restarts, conflicts, decisions, and propagations

Usage example:

>>> formula = PCNF(from_file="some-file.qdimacs")
>>> solver = DepQBF()
>>> solver.solve()
>>> print(solver.get_stats())
{'restarts': 2, 'conflicts': 0, 'decisions': 254, 'propagations': 2321}        

solve(formula)#

Interface method for solving a PCNF-formula with the solver

Parameters:: formula (pyqbf.formula.PCNF) – a formula to be solved
Returns:: True, if the formula is SAT, else False
Return type:: bool

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> solver = QFun()
>>> print(solver.solve(pcnf))
True            

pyqbf.solvers.solve(formula)#

Providing the most basic functionality one would expect: solving the given formula. If the only goal is solving a provided formula without thinking about which solver or configuration, this function may be used.

Parameters:: formula (pyqbf.formula.PCNF) – the formula to be solve
Returns:: True if the formula is satisfiable
Return type:: bool

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> print(solve(pcnf))
True            

pyqbf.solvers.solve_all_files(targets)#

Loads the formulas from a given list of targets and solves them.

Parameters:: target (list[str]) – a list of paths to the formulas
Returns:: A dictionary containing the corresponding result from solving
Return type:: dict[str,bool]

Usage example:

>>> targets = ["some-file.qdimacs", "some-other-file.qdimacs", "another-file.qdimacs"]
>>> print(solve_all_files(targets))
{"some-file.qdimacs": True, "some-other-file.qdimacs": False, "another-file.qdimacs": True}

pyqbf.solvers.solve_file(target)#

Loads the formula from a given target and solves it.

Parameters:: target (str) – a path to the formula
Returns:: True if the formula provided in the file is satisfiable
Return type:: bool

Usage example:

>>> print(solve_file("some-file.qdimacs"))
True      

QBF solver’s API (pyqbf.solvers)#

List of classes#

List of methods#

List of constants#

Module description#

Module details#

QBF solver’s API (`pyqbf.solvers`)#