SAT solvers’ API (pysat.solvers
)¶
List of classes¶
This class serves to determine the solver requested by a user given a string name. |
|
Main class for creating and manipulating a SAT solver. |
|
|
CaDiCaL SAT solver. |
|
Glucose 3 SAT solver. |
|
Glucose 4.1 SAT solver. |
|
Lingeling SAT solver. |
|
MapleLCMDistChronoBT SAT solver. |
|
MapleCM SAT solver. |
|
MapleCOMSPS_LRB SAT solver. |
|
Minicard SAT solver. |
|
MiniSat 2.2 SAT solver. |
|
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)
Lingeling (bbc-9230380-160707)
MapleLCMDistChronoBT (SAT competition 2018 version)
MapleCM (SAT competition 2018 version)
Maplesat (MapleCOMSPS_LRB)
Minicard (1.2)
Minisat (2.2 release)
Minisat (GitHub version)
All solvers can be accessed through a unified MiniSat-like 1 incremental 2 interface described below.
- 1
Niklas Eén, Niklas Sörensson. An Extensible SAT-solver. SAT 2003. pp. 502-518
- 2(1,2)
Niklas Eén, Niklas Sörensson. Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4). 2003. pp. 543-560
The module provides direct access to all supported solvers using the
corresponding classes Glucose3
, Glucose4
,
Lingeling
, MapleChrono
, MapleCM
,
Maplesat
, 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 Cadical
,
Glucose3
, Glucose4
, Lingeling
,
MapleChrono
, MapleCM
, Maplesat
,
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 ‘cadical’, ‘glucose3’, ‘glucose4’, ‘lingeling’, ‘maplechrono’, ‘maplecm’, ‘maplesat’, ‘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 argumentname
, while all the others are default. This means that explicit solver constructors, e.g.Glucose3
orMinisatGH
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
, theuse_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 thewith
statement, deletion is done automatically when the end of thewith
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
anduse_timer
, solversCadical
,Lingeling
,Glucose3
,Glucose4
,MapleChrono
,MapleCM
andMaplesat
can have additional default arguments. One such argument supported byGlucose3
andGlucose4
but also byCadical
,Lingeling
,MapleChrono
,MapleCM
, andMaplesat
is DRUP proof logging. This can be enabled by setting thewith_proof
argument toTrue
(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 and in contrast to
Cadical
andLingeling
, bothGlucose3
andGlucose4
have one more default argumentincr
(False
by default), which enables incrementality features introduced in Glucose3 3. To summarize, the additional arguments of Glucose are:- Parameters
incr (bool) – enable the incrementality features of Glucose3 3.
with_proof (bool) – enable proof logging in the DRUP format.
- 3(1,2)
Gilles Audemard, Jean-Marie Lagniez, Laurent Simon. Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. SAT 2013. pp. 309-317
-
add_atmost
(lits, k, no_return=True)¶ This method is responsible for adding a new native AtMostK (see
pysat.card
) constraint intoMinicard
.Note that none of the other solvers supports 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
andk
, wherelits
is a list of literals in the sum.- Parameters
lits (iterable(int)) – a list of literals.
k (int) – upper bound on the number of satisfied 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 toFalse
.
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 toFalse
.
Note that a clause can be either a
list
of integers or another iterable type over integers, e.g.tuple
orset
among others.A usage example is the following:
>>> s = Solver(bootstrap_with=[[-1, 2], [-1, -2]]) >>> s.add_clause([1], no_return=False) False
-
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 toTrue
by default.- Return type
bool if
no_return
is set toFalse
.
>>> 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 abudget
variable and is an integer greater than0
. If the budget is set to0
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()
-
delete
()¶ Solver destructor, which must be called explicitly if the solver is to be removed. This is not needed inside an
with
block.
-
enum_models
(assumptions=[])¶ This method can be used to enumerate models of a CNF formula. It can be used as a standard Python iterator. The method can be used without arguments but also with an argument
assumptions
, which is a list of literals to “assume”.- 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.
-
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 (seeclear_interrupt()
).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()) None >>> m.delete()
-
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. SeeSolver
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
-
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 abudget
variable and is an integer greater than0
. If the budget is set to0
or-1
, the upper bound on the number of conflicts 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 isFalse
. Additionally, a user may specify an optional argumentphase_saving
(0
by default) to enable MiniSat-like phase saving.Note that only MiniSat-like solvers support this functionality (e.g.
Cadical
andLingeling
do not support it).- Parameters
assumptions (iterable(int)) – a list of assumption literals.
phase_saving (int) – enable phase saving (can be
0
,1
, and2
).
- 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()
-
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
andLingeling
will always respect them when branching on these variables. However, solversGlucose3
,Glucose4
,MapleChrono
,MapleCM
,Maplesat
,Minisat22
, andMinicard
can redefine the preferences in any of the following SAT calls due to the phase saving heuristic.Also note that
Cadical
does 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()
andappend_formula()
). Unless interrupted with SIGINT, the method returns eitherTrue
orFalse
.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=[])¶ This method is used to check satisfiability of a CNF formula given to the solver (see methods
add_clause()
andappend_formula()
), taking into account the upper bounds on the number of conflicts (seeconf_budget()
) and the number of propagations (seeprop_budget()
). If the number of conflicts or propagations is set to be larger than 0 then the following SAT call done withsolve_limited()
will not exceed these values, i.e. it will be incomplete. Otherwise, such a call will be identical tosolve()
.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 returnsTrue
orFalse
.Note that only MiniSat-like solvers support this functionality (e.g.
Cadical
andLingeling
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.)- Parameters
assumptions (iterable(int)) – a list of assumption literals.
- 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/orprop_budget()
, limited SAT calls support deterministic and non-deterministic interruption from inside a Python script. See theinterrupt()
andclear_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
-
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 toTrue
when creating the solver (seeSolver
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 toTrue
when creating the solver (seeSolver
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.
cadical = ('cd', 'cdl', 'cadical') glucose3 = ('g3', 'g30', 'glucose3', 'glucose30') glucose4 = ('g4', 'g41', 'glucose4', 'glucose41') lingeling = ('lgl', 'lingeling') maplechrono = ('mcb', 'chrono', 'maplechrono') maplecm = ('mcm', 'maplecm') maplesat = ('mpl', 'maple', 'maplesat') 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.