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.

Cadical

CaDiCaL SAT solver.

Gluecard3

Gluecard 3 SAT solver.

Gluecard4

Gluecard 4 SAT solver.

Glucose3

Glucose 3 SAT solver.

Glucose4

Glucose 4.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:

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

  • Gluecard3

  • Gluecard4

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 Cadical, 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 Cadical, Gluecard3, Gluecard4, Glucose3, Glucose4, 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 ‘cadical’, ‘gluecard3’, ‘gluecard4’, ‘glucose3’, ‘glucose4’, ‘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 Cadical, Lingeling, Gluecard3, Gluecard4, Glucose3, Glucose4, 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, Gluecard3, and Gluecard4 have one more default argument incr (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

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}
add_atmost(lits, k, 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.

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 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
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()
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 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”.

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.

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()
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
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 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 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. Cadical 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()
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 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() 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. Cadical 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
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.

cadical     = ('cd', 'cdl', 'cadical')
gluecard3   = ('gc3', 'gc30', 'gluecard3', 'gluecard30')
gluecard41  = ('gc3', 'gc41', 'gluecard4', 'gluecard41')
glucose3    = ('g3', 'g30', 'glucose3', 'glucose30')
glucose4    = ('g4', 'g41', 'glucose4', 'glucose41')
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.