SAT solvers’ API (`pysat.solvers`)#

List of classes#

`SolverNames`	This class serves to determine the solver requested by a user given a string name.
`Solver`	Main class for creating and manipulating a SAT solver.
`Cadical103`	CaDiCaL 1.0.3 SAT solver.
`Cadical153`	CaDiCaL 1.5.3 SAT solver.
`Cadical195`	CaDiCaL 1.9.5 SAT solver.
`CryptoMinisat`	CryptoMinisat solver accessed through `pycryptosat` package.
`Gluecard3`	Gluecard 3 SAT solver.
`Gluecard4`	Gluecard 4 SAT solver.
`Glucose3`	Glucose 3 SAT solver.
`Glucose4`	Glucose 4.1 SAT solver.
`Glucose42`	Glucose 4.2.1 SAT solver.
`Lingeling`	Lingeling SAT solver.
`MapleChrono`	MapleLCMDistChronoBT SAT solver.
`MapleCM`	MapleCM SAT solver.
`Maplesat`	MapleCOMSPS_LRB SAT solver.
`Mergesat3`	MergeSat 3 SAT solver.
`Minicard`	Minicard SAT solver.
`Minisat22`	MiniSat 2.2 SAT solver.
`MinisatGH`	MiniSat SAT solver (version from github).

Module description#

This module provides incremental access to a few modern SAT solvers. The solvers supported by PySAT are:

CaDiCaL (rel-1.0.3)
Glucose (3.0)
Glucose (4.1)
Glucose (4.2.1)
Lingeling (bbc-9230380-160707)
MapleLCMDistChronoBT (SAT competition 2018 version)
MapleCM (SAT competition 2018 version)
Maplesat (MapleCOMSPS_LRB)
Mergesat (3.0)
Minicard (1.2)
Minisat (2.2 release)
Minisat (GitHub version)

Additionally, PySAT includes the versions of Glucose3 and Glucose4 that support native cardinality constraints, ported from Minicard:

Gluecard3
Gluecard4

Finally, PySAT offers rudimentary support of CryptoMiniSat5 [3] through the interface provided by the pycryptosat package. The functionality is exposed via the class CryptoMinisat. Note that the solver currently implements only the basic functionality, i.e. adding clauses and XOR-clauses as well as making (incremental) SAT calls.

All solvers can be accessed through a unified MiniSat-like [1] incremental [2] interface described below.

The module provides direct access to all supported solvers using the corresponding classes Cadical103, Cadical153, Cadical195, CryptoMinisat, Gluecard3, Gluecard4, Glucose3, Glucose4, Lingeling, MapleChrono, MapleCM, Maplesat, Mergesat3, Minicard, Minisat22, and MinisatGH. However, the solvers can also be accessed through the common base class Solver using the solver name argument. For example, both of the following pieces of code create a copy of the Glucose3 solver:

>>> from pysat.solvers import Glucose3, Solver
>>>
>>> g = Glucose3()
>>> g.delete()
>>>
>>> s = Solver(name='g3')
>>> s.delete()

The pysat.solvers module is designed to create and manipulate SAT solvers as oracles, i.e. it does not give access to solvers’ internal parameters such as variable polarities or activities. PySAT provides a user with the following basic SAT solving functionality:

creating and deleting solver objects
adding individual clauses and formulas to solver objects
making SAT calls with or without assumptions
propagating a given set of assumption literals
setting preferred polarities for a (sub)set of variables
extracting a model of a satisfiable input formula
enumerating models of an input formula
extracting an unsatisfiable core of an unsatisfiable formula
extracting a DRUP proof logged by the solver

PySAT supports both non-incremental and incremental SAT solving. Incrementality can be achieved with the use of the MiniSat-like assumption-based interface [2]. It can be helpful if multiple calls to a SAT solver are needed for the same formula using different sets of “assumptions”, e.g. when doing consecutive SAT calls for formula \(\mathcal{F}\land (a_{i_1}\land\ldots\land a_{i_1+j_1})\) and \(\mathcal{F}\land (a_{i_2}\land\ldots\land a_{i_2+j_2})\), where every \(a_{l_k}\) is an assumption literal.

There are several advantages of using assumptions: (1) it enables one to keep and reuse the clauses learnt during previous SAT calls at a later stage and (2) assumptions can be easily used to extract an unsatisfiable core of the formula. A drawback of assumption-based SAT solving is that the clauses learnt are longer (they typically contain many assumption literals), which makes the SAT calls harder.

In PySAT, assumptions should be provided as a list of literals given to the solve() method:

>>> from pysat.solvers import Solver
>>> s = Solver()
>>>
... # assume that solver s is fed with a formula
>>>
>>> s.solve()  # a simple SAT call
True
>>>
>>> s.solve(assumptions=[1, -2, 3])  # a SAT call with assumption literals
False
>>> s.get_core()  # extracting an unsatisfiable core
[3, 1]

In order to shorten the description of the module, the classes providing direct access to the individual solvers, i.e. classes Cadical103, Cadical153, Cadical195, CryptoMinisat, Gluecard3, Gluecard4, Glucose3, Glucose4, Glucose42, Lingeling, MapleChrono, MapleCM, Maplesat, Mergesat3, Minicard, Minisat22, and MinisatGH, are omitted. They replicate the interface of the base class Solver and, thus, can be used the same exact way.

Module details#

exception pysat.solvers.NoSuchSolverError#

This exception is raised when creating a new SAT solver whose name does not match any name in SolverNames. The list of known solvers includes the names ‘cadical103’, ‘cadical153’, ‘cadical195’, ‘cryptosat’, ‘gluecard3’, ‘gluecard4’, ‘glucose3’, ‘glucose4’, glucose42, ‘lingeling’, ‘maplechrono’, ‘maplecm’, ‘maplesat’, ‘mergesat3’, ‘minicard’, ‘minisat22’, and ‘minisatgh’.

with_traceback()#: Exception.with_traceback(tb) – set self.__traceback__ to tb and return self.

class pysat.solvers.Solver(name='m22', bootstrap_with=None, use_timer=False, **kwargs)#

Main class for creating and manipulating a SAT solver. Any available SAT solver can be accessed as an object of this class and so Solver can be seen as a wrapper for all supported solvers.

The constructor of Solver has only one mandatory argument name, while all the others are default. This means that explicit solver constructors, e.g. Glucose3 or MinisatGH etc., have only default arguments.

Parameters:

name (str) – solver’s name (see SolverNames).
bootstrap_with (iterable(iterable(int))) – a list of clauses for solver initialization.
use_timer (bool) – whether or not to measure SAT solving time.

The bootstrap_with argument is useful when there is an input CNF formula to feed the solver with. The argument expects a list of clauses, each clause being a list of literals, i.e. a list of integers.

If set to True, the use_timer parameter will force the solver to accumulate the time spent by all SAT calls made with this solver but also to keep time of the last SAT call.

Once created and used, a solver 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.

Given the above, a couple of examples of solver creation are the following:

>>> from pysat.solvers import Solver, Minisat22
>>>
>>> s = Solver(name='g4')
>>> s.add_clause([-1, 2])
>>> s.add_clause([-1, -2])
>>> s.solve()
True
>>> print(s.get_model())
[-1, -2]
>>> s.delete()
>>>
>>> with Minisat22(bootstrap_with=[[-1, 2], [-1, -2]]) as m:
...     m.solve()
True
...     print(m.get_model())
[-1, -2]

Note that while all explicit solver classes necessarily have default arguments bootstrap_with and use_timer, solvers Cadical103, Cadical153, Cadical195, Lingeling, Gluecard3, Gluecard4, Glucose3, Glucose4, Glucose42, MapleChrono, MapleCM, and Maplesat can have additional default arguments. One such argument supported by is DRUP proof logging. This can be enabled by setting the with_proof argument to True (False by default):

>>> from pysat.solvers import Lingeling
>>> from pysat.examples.genhard import PHP
>>>
>>> cnf = PHP(nof_holes=2)  # pigeonhole principle for 3 pigeons
>>>
>>> with Lingeling(bootstrap_with=cnf.clauses, with_proof=True) as l:
...     l.solve()
False
...     l.get_proof()
['-5 0', '6 0', '-2 0', '-4 0', '1 0', '3 0', '0']

Additionally, Glucose-based solvers, namely Glucose3, Glucose4, Glucose42, Gluecard3, and Gluecard4 have one more default argument incr (False by default), which enables incrementality features introduced in Glucose3 [4]. To summarize, the additional arguments of Glucose are:

Parameters:

incr (bool) – enable the incrementality features of Glucose3 [4].
with_proof (bool) – enable proof logging in the DRUP format.

Finally, most MiniSat-based solvers can be exploited in the “warm-start” mode in the case of satisfiable formulas. This may come in handy in various model enumeration settings. Note that warm-start mode is disabled in the case of limited solving with “unknown” outcomes. Warm-start mode can be set with the use of the warm_start parameter:

Parameters:: warm_start (bool) – use the solver in the “warm-start” mode

accum_stats()#

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

Return type:: dict.

Example:

>>> from pysat.examples.genhard import PHP
>>> cnf = PHP(5)
>>> from pysat.solvers import Solver
>>> with Solver(bootstrap_with=cnf) as s:
...     print(s.solve())
...     print(s.accum_stats())
False
{'restarts': 2, 'conflicts': 201, 'decisions': 254, 'propagations': 2321}

activate_atmost()#: Activate native linear (cardinality or pseudo-Boolean) constraint reasoning. This is supported only by Cadical195 by means of its external propagators functionality and the use of BooleanEngine.

Note

IPASIR-UP related. Cadical195 only.

add_atmost(lits, k, weights=[], no_return=True)#

This method is responsible for adding a new native AtMostK (see pysat.card) constraint.

Note that most of the solvers do not support native AtMostK constraints.

An AtMostK constraint is \(\sum_{i=1}^{n}{x_i}\leq k\). A native AtMostK constraint should be given as a pair lits and k, where lits is a list of literals in the sum.

Also, besides unweighted AtMostK constraints, some solvers (see Cadical195) support their weighted counterparts, i.e. pseudo-Boolean constraints of the form \(\sum_{i=1}^{n}{w_i \cdot x_i}\leq k\). The weights of the literals can be specified using the argument weights.

Parameters:

lits (iterable(int)) – a list of literals
k (int) – upper bound on the number of satisfied literals
weights (list(int)) – a list of weights
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.

A usage example is the following:

>>> s = Solver(name='mc', bootstrap_with=[[1], [2], [3]])
>>> s.add_atmost(lits=[1, 2, 3], k=2, no_return=False)
False
>>> # the AtMostK constraint is in conflict with initial unit clauses

add_clause(clause, no_return=True)#

This method is used to add a single clause to the solver. An 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.

Note that a clause can be either a list of integers or another iterable type over integers, e.g. tuple or set among others.

A usage example is the following:

>>> s = Solver(bootstrap_with=[[-1, 2], [-1, -2]])
>>> s.add_clause([1], no_return=False)
False

add_xor_clause(lits, value=True)#

Add a new XOR clause to solver’s internal formula. The input parameters include the list of literals and the right-hand side (the value of the sum).

Note that XOR clauses are currently supported only by CryptoMinisat.

Parameters:

lits (iterable(int)) – list of literals in the clause (left-hand side)
value (bool) – value of the sum (right-hand-side)

A usage example is the following:

>>> from pysat.solvers import Solver
>>> with Solver(name='cms', bootstrap_with=[[1, 3]]) as solver:
...     solver.add_xor_clause(lits=[1, 2], value=True)
...     for model in solver.enum_models():
...         print(model)
...
[-1, 2, 3]
[1, -2, 3]
[1, -2, -3]

append_formula(formula, no_return=True)#

This method can be used to add a given list of clauses into the solver.

Parameters:

formula (iterable(iterable(int))) – a list of clauses.
no_return (bool) – check solver’s internal formula and return the result, if set to False.

The no_return argument is set to True by default.

Return type:: bool if no_return is set to False.

>>> cnf = CNF()
... # assume the formula contains clauses
>>> s = Solver()
>>> s.append_formula(cnf.clauses, no_return=False)
True

clear_interrupt()#: Clears a previous interrupt. If a limited SAT call was interrupted using the interrupt() method, this method must be called before calling the SAT solver again.

conf_budget(budget=- 1)#

Set limit (i.e. the upper bound) on the number of conflicts in the next limited SAT call (see solve_limited()). The limit value is given as a budget variable and is an integer greater than 0. If the budget is set to 0 or -1, the upper bound on the number of conflicts is disabled.

Parameters:: budget (int) – the upper bound on the number of conflicts.

Example:

>>> from pysat.solvers import MinisatGH
>>> from pysat.examples.genhard import PHP
>>>
>>> cnf = PHP(nof_holes=20)  # PHP20 is too hard for a SAT solver
>>> m = MinisatGH(bootstrap_with=cnf.clauses)
>>>
>>> m.conf_budget(2000)  # getting at most 2000 conflicts
>>> print(m.solve_limited())  # making a limited oracle call
None
>>> m.delete()

configure(parameters)#

Configure Cadical153 or Cadical195 by setting some of the predefined parameters to selected values. Note that this method can be invoked only for Cadical153 and Cadical195 – no other solvers support this for now.

Also note that this call must follow the creation of the new solver object; otherwise, an exception may be thrown.

The list of available options of Cadical153 and Cadical195 and the corresponding values they can be assigned to is provided here.

Parameters:: parameters (dict) – parameter names mapped to integer values

connect_propagator(propagator)#: Attach an external propagator through the IPASIR-UP interface. The only expected argument is propagator, which must be an object of a class inheriting from the abstract class Propagator.

Note

IPASIR-UP related. Cadical195 only.

dec_budget(budget)#

Set limit (i.e. the upper bound) on the number of decisions in the next limited SAT call (see solve_limited()). The limit value is given as a budget variable and is an integer greater than 0. If the budget is set to 0 or -1, the upper bound on the number of decisions is disabled.

Note that this functionality is supported by Cadical103, Cadical153, and Cadical195 only!

Parameters:: budget (int) – the upper bound on the number of decisions.

Example:

>>> from pysat.solvers import Cadical153
>>> from pysat.examples.genhard import Parity
>>>
>>> cnf = Parity(size=10)  # too hard for a SAT solver
>>> c = Cadical153(bootstrap_with=cnf.clauses)
>>>
>>> c.dec_budget(500)  # doing at most 500 decisions
>>> print(c.solve_limited())  # making a limited oracle call
None
>>> c.delete()

delete()#: Solver destructor, which must be called explicitly if the solver is to be removed. This is not needed inside an with block.

disable_propagator()#: Ask the solver to disable the propagator on the fly. This will it in passive mode, i.e. it will be invoked only to check assignments found by the solver.

Note

IPASIR-UP related. Cadical195 only.

disconnect_propagator()#: Disconnect the previously attached propagator. This will also reset all the variables marked in the solver as observed by the propagator.

Note

IPASIR-UP related. Cadical195 only.

enable_propagator()#: Ask the solver to enable the propagator on the fly. This will put it in active mode.

Note

IPASIR-UP related. Cadical195 only.

enum_models(assumptions=[])#

This method can be used to enumerate models of a CNF formula and it performs as a standard Python iterator. The method can be called without arguments but also with an argument assumptions, which represents a list of literals to “assume”.

Note that the method expects the list of assumption literals (if any) to contain no duplicate literals. Otherwise, it is not guaranteed to run correctly. As such, a user is recommended to explicitly filter out duplicate literals from the assumptions list before calling solve(), solve_limited(), propagate(), or enum_models().

Warning

Once finished, model enumeration results in the target formula being unsatisfiable. This is because the enumeration process blocks each previously computed model by adding a new clause until no more models of the formula exist.

Parameters:: assumptions (iterable(int)) – a list of assumption literals.
Return type:: list(int).

Example:

>>> with Solver(bootstrap_with=[[-1, 2], [-2, 3]]) as s:
...     for m in s.enum_models():
...         print(m)
[-1, -2, -3]
[-1, -2, 3]
[-1, 2, 3]
[1, 2, 3]
>>>
>>> with Solver(bootstrap_with=[[-1, 2], [-2, 3]]) as s:
...     for m in s.enum_models(assumptions=[1]):
...         print(m)
[1, 2, 3]

get_core()#

This method is to be used for extracting an unsatisfiable core in the form of a subset of a given set of assumption literals, which are responsible for unsatisfiability of the formula. This can be done only if the previous SAT call returned False (UNSAT). Otherwise, None is returned.

Return type:: list(int) or None.

Usage example:

>>> from pysat.solvers import Minisat22
>>> m = Minisat22()
>>> m.add_clause([-1, 2])
>>> m.add_clause([-2, 3])
>>> m.add_clause([-3, 4])
>>> m.solve(assumptions=[1, 2, 3, -4])
False
>>> print(m.get_core())  # literals 2 and 3 are not in the core
[-4, 1]
>>> m.delete()

get_model()#

The method is to be used for extracting a satisfying assignment for a CNF formula given to the solver. A model is provided if a previous SAT call returned True. Otherwise, None is reported.

Return type:: list(int) or None.

Example:

>>> from pysat.solvers import Solver
>>> s = Solver()
>>> s.add_clause([-1, 2])
>>> s.add_clause([-1, -2])
>>> s.add_clause([1, -2])
>>> s.solve()
True
>>> print(s.get_model())
[-1, -2]
>>> s.delete()

get_proof()#

A DRUP proof can be extracted using this method if the solver was set up to provide a proof. Otherwise, the method returns None.

Return type:: list(str) or None.

Example:

>>> from pysat.solvers import Solver
>>> from pysat.examples.genhard import PHP
>>>
>>> cnf = PHP(nof_holes=3)
>>> with Solver(name='g4', with_proof=True) as g:
...     g.append_formula(cnf.clauses)
...     g.solve()
False
...     print(g.get_proof())
['-8 4 1 0', '-10 0', '-2 0', '-4 0', '-8 0', '-6 0', '0']

get_status()#

The result of a previous SAT call is stored in an internal variable and can be later obtained using this method.

Return type:: Boolean or None.

None is returned if a previous SAT call was interrupted.

ignore(var)#: Inform the solver that a given variable is ignored by the propagator attached to it.

Note

IPASIR-UP related. Cadical195 only.

interrupt()#

Interrupt the execution of the current limited SAT call (see solve_limited()). Can be used to enforce time limits using timer objects. The interrupt must be cleared before performing another SAT call (see clear_interrupt()).

Note that this method can be called if limited SAT calls are made with the option expect_interrupt set to True.

Behaviour is undefined if used to interrupt a non-limited SAT call (see solve()).

Example:

>>> from pysat.solvers import MinisatGH
>>> from pysat.examples.genhard import PHP
>>> from threading import Timer
>>>
>>> cnf = PHP(nof_holes=20)  # PHP20 is too hard for a SAT solver
>>> m = MinisatGH(bootstrap_with=cnf.clauses)
>>>
>>> def interrupt(s):
>>>     s.interrupt()
>>>
>>> timer = Timer(10, interrupt, [m])
>>> timer.start()
>>>
>>> print(m.solve_limited(expect_interrupt=True))
None
>>> m.delete()

is_decision(lit)#: Check whether a given literal that is currently observed by the attached propagator is a assigned a value by branching or by propagation, i.e. whether it is decision or not. In the former case, the method returns True; otherwise, it returns False.

Note

IPASIR-UP related. Cadical195 only.

new(name='m22', bootstrap_with=None, use_timer=False, **kwargs)#

The actual solver constructor invoked from __init__(). Chooses the solver to run, based on its name. See Solver for the parameters description.

Raises:: NoSuchSolverError – if there is no solver matching the given name.

nof_clauses()#

This method returns the number of clauses currently appearing in the formula given to the solver.

Return type:: int.

Example:

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

nof_vars()#

This method returns the number of variables currently appearing in the formula given to the solver.

Return type:: int.

Example:

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

observe(var)#: Inform the solver that a given variable is observed by the propagator attached to it.

Note

IPASIR-UP related. Cadical195 only.

prop_budget(budget=- 1)#

Set limit (i.e. the upper bound) on the number of propagations in the next limited SAT call (see solve_limited()). The limit value is given as a budget variable and is an integer greater than 0. If the budget is set to 0 or -1, the upper bound on the number of propagations is disabled.

Parameters:: budget (int) – the upper bound on the number of propagations.

Example:

>>> from pysat.solvers import MinisatGH
>>> from pysat.examples.genhard import Parity
>>>
>>> cnf = Parity(size=10)  # too hard for a SAT solver
>>> m = MinisatGH(bootstrap_with=cnf.clauses)
>>>
>>> m.prop_budget(100000)  # doing at most 100000 propagations
>>> print(m.solve_limited())  # making a limited oracle call
None
>>> m.delete()

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

The method takes a list of assumption literals and does unit propagation of each of these literals consecutively. A Boolean status is returned followed by a list of assigned (assumed and also propagated) literals. The status is True if no conflict arised during propagation. Otherwise, the status is False. Additionally, a user may specify an optional argument phase_saving (0 by default) to enable MiniSat-like phase saving.

Note that only MiniSat-like solvers support this functionality (e.g. Cadical103, class:Cadical153, Cadical195, and Lingeling do not support it).

Parameters:

assumptions (iterable(int)) – a list of assumption literals.
phase_saving (int) – enable phase saving (can be 0, 1, and 2).

Return type:

tuple(bool, list(int)).

Usage example:

>>> from pysat.solvers import Glucose3
>>> from pysat.card import *
>>>
>>> cnf = CardEnc.atmost(lits=range(1, 6), bound=1, encoding=EncType.pairwise)
>>> g = Glucose3(bootstrap_with=cnf.clauses)
>>>
>>> g.propagate(assumptions=[1])
(True, [1, -2, -3, -4, -5])
>>>
>>> g.add_clause([2])
>>> g.propagate(assumptions=[1])
(False, [])
>>>
>>> g.delete()

propagator_active()#: Check if the propagator is currently active or passive. In the former case, the method will return True; otherwise, it will return False.

Note

IPASIR-UP related. Cadical195 only.

reset_observed()#: Ask the solver to reset all observed variables.

Note

IPASIR-UP related. Cadical195 only.

set_phases(literals=[])#

The method takes a list of literals as an argument and sets phases (or MiniSat-like polarities) of the corresponding variables respecting the literals. For example, if a given list of literals is [1, -513], the solver will try to set variable \(x_1\) to true while setting \(x_{513}\) to false.

Note that once these preferences are specified, MinisatGH and Lingeling will always respect them when branching on these variables. However, solvers Glucose3, Glucose4, MapleChrono, MapleCM, Maplesat, Minisat22, and Minicard can redefine the preferences in any of the following SAT calls due to the phase saving heuristic.

Also note that Cadical103, Cadical153, and Cadical195 do not support this functionality.

Parameters:: literals (iterable(int)) – a list of literals.

Usage example:

>>> from pysat.solvers import Glucose3
>>>
>>> g = Glucose3(bootstrap_with=[[1, 2]])
>>> # the formula has 3 models: [-1, 2], [1, -2], [1, 2]
>>>
>>> g.set_phases(literals=[1, 2])
>>> g.solve()
True
>>> g.get_model()
[1, 2]
>>>
>>> g.delete()

solve(assumptions=[])#

This method is used to check satisfiability of a CNF formula given to the solver (see methods add_clause() and append_formula()). Unless interrupted with SIGINT, the method returns either True or False.

Incremental SAT calls can be made with the use of assumption literals. (Note that the assumptions argument is optional and disabled by default.)

Parameters:: assumptions (iterable(int)) – a list of assumption literals.
Return type:: Boolean or None.

Example:

>>> from pysat.solvers import Solver
>>> s = Solver(bootstrap_with=[[-1, 2], [-2, 3])
>>> s.solve()
True
>>> s.solve(assumptions=[1, -3])
False
>>> s.delete()

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

This method is used to check satisfiability of a CNF formula given to the solver (see methods add_clause() and append_formula()), taking into account the upper bounds on the number of conflicts (see conf_budget()) and the number of propagations (see prop_budget()). If the number of conflicts or propagations is set to be larger than 0 then the following SAT call done with solve_limited() will not exceed these values, i.e. it will be incomplete. Otherwise, such a call will be identical to solve().

As soon as the given upper bound on the number of conflicts or propagations is reached, the SAT call is dropped returning None, i.e. unknown. None can also be returned if the call is interrupted by SIGINT. Otherwise, the method returns True or False.

Note that only MiniSat-like solvers support this functionality (e.g. Cadical103, Cadical153, Cadical195, and Lingeling do not support it).

Incremental SAT calls can be made with the use of assumption literals. (Note that the assumptions argument is optional and disabled by default.)

Note that since SIGINT handling and interrupt() are not configured to work together at this point, additional input parameter expect_interrupt is assumed to be given, indicating what kind of interruption may happen during the execution of solve_limited(): whether a SIGINT signal or internal interrupt(). By default, a SIGINT signal handling is assumed. If expect_interrupt is set to True and eventually a SIGINT is received, the behavior is undefined.

Parameters:

assumptions (iterable(int)) – a list of assumption literals.
expect_interrupt (bool) – whether interrupt() will be called

Return type:

Boolean or None.

Doing limited SAT calls can be of help if it is known that complete SAT calls are too expensive. For instance, it can be useful when minimizing unsatisfiable cores in MaxSAT (see pysat.examples.RC2.minimize_core() also shown below).

Also and besides supporting deterministic interruption based on conf_budget() and/or prop_budget(), limited SAT calls support deterministic and non-deterministic interruption from inside a Python script. See the interrupt() and clear_interrupt() methods for details.

Usage example:

... # assume that a SAT oracle is set up to contain an unsatisfiable
... # formula, and its core is stored in variable "core"
oracle.conf_budget(1000)  # getting at most 1000 conflicts be call

i = 0
while i < len(core):
    to_test = core[:i] + core[(i + 1):]

    # doing a limited call
    if oracle.solve_limited(assumptions=to_test) == False:
        core = to_test
    else:  # True or *unknown*
        i += 1

start_mode(warm=False)#

Set start mode: either warm or standard. Warm start mode can be beneficial if one is interested in efficient model enumeration.

Note that warm start mode is disabled in the case of limited solving with “unknown” outcomes. Moreover, warm start mode may lead to unexpected results in case of assumption-based solving with a varying list of assumption literals.

Example:

>>> def model_count(solver, formula, vlimit=None, warm_start=False):
...     with Solver(name=solver, bootstrap_with=formula, use_timer=True, warm_start=warm_start) as oracle:
...         count = 0
...         while oracle.solve() == True:
...             model = oracle.get_model()
...             if vlimit:
...                 model = model[:vlimit]
...             oracle.add_clause([-l for l in model])
...             count += 1
...         print('{0} models in {1:.4f}s'.format(count, oracle.time_accum()))
>>>
>>> model_count('mpl', cnf, vlimit=16, warm_start=False)
58651 models in 7.9903s
>>> model_count('mpl', cnf, vlimit=16, warm_start=True)
58651 models in 0.3951s

supports_atmost()#

This method can be called to determine whether the solver supports native AtMostK (see pysat.card) constraints.

Return type:: bool

A usage example is the following:

>>> s = Solver(name='mc')
>>> s.supports_atmost()
True
>>> # there is support for AtMostK constraints in this solver

time()#

Get the time spent when doing the last SAT call. Note that the time is measured only if the use_timer argument was previously set to True when creating the solver (see Solver for details).

Return type:: float.

Example usage:

>>> from pysat.solvers import Solver
>>> from pysat.examples.genhard import PHP
>>>
>>> cnf = PHP(nof_holes=10)
>>> with Solver(bootstrap_with=cnf.clauses, use_timer=True) as s:
...     print(s.solve())
False
...     print('{0:.2f}s'.format(s.time()))
150.16s

time_accum()#

Get the time spent for doing all SAT calls accumulated. Note that the time is measured only if the use_timer argument was previously set to True when creating the solver (see Solver for details).

Return type:: float.

Example usage:

>>> from pysat.solvers import Solver
>>> from pysat.examples.genhard import PHP
>>>
>>> cnf = PHP(nof_holes=10)
>>> with Solver(bootstrap_with=cnf.clauses, use_timer=True) as s:
...     print(s.solve(assumptions=[1]))
False
...     print('{0:.2f}s'.format(s.time()))
1.76s
...     print(s.solve(assumptions=[-1]))
False
...     print('{0:.2f}s'.format(s.time()))
113.58s
...     print('{0:.2f}s'.format(s.time_accum()))
115.34s

class pysat.solvers.SolverNames#

This class serves to determine the solver requested by a user given a string name. This allows for using several possible names for specifying a solver.

cadical103  = ('cd', 'cd103', 'cdl', 'cdl103', 'cadical103')
cadical153  = ('cd15', 'cd153', 'cdl15', 'cdl153', 'cadical153')
cadical195  = ('cd19', 'cd195', 'cdl19', 'cdl195', 'cadical195')
cryptosat   = ('cms', 'cms5', 'crypto', 'crypto5', 'cryptominisat', 'cryptominisat5')
gluecard3   = ('gc3', 'gc30', 'gluecard3', 'gluecard30')
gluecard41  = ('gc4', 'gc41', 'gluecard4', 'gluecard41')
glucose3    = ('g3', 'g30', 'glucose3', 'glucose30')
glucose4    = ('g4', 'g41', 'glucose4', 'glucose41')
glucose42   = ('g42', 'g421', 'glucose42', 'glucose421')
lingeling   = ('lgl', 'lingeling')
maplechrono = ('mcb', 'chrono', 'maplechrono')
maplecm     = ('mcm', 'maplecm')
maplesat    = ('mpl', 'maple', 'maplesat')
mergesat3   = ('mg3', 'mgs3', 'mergesat3', 'mergesat30')
minicard    = ('mc', 'mcard', 'minicard')
minisat22   = ('m22', 'msat22', 'minisat22')
minisatgh   = ('mgh', 'msat-gh', 'minisat-gh')

As a result, in order to select Glucose3, a user can specify the solver’s name: either 'g3', 'g30', 'glucose3', or 'glucose30'. Note that the capitalized versions of these names are also allowed.

Formula processing (pysat.process)

Fu&Malik MaxSAT algorithm (pysat.examples.fm)

SAT solvers’ API (pysat.solvers)#

List of classes#

Module description#

Module details#

SAT solvers’ API (`pysat.solvers`)#