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:
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
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:
>>> frompysat.solversimportSolver>>> s=Solver()>>>... # assume that solver s is fed with a formula>>>>>> s.solve()# a simple SAT callTrue>>>>>> s.solve(assumptions=[1,-2,3])# a SAT call with assumption literalsFalse>>> 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.
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’.
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.
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:
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):
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
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.
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
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.
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.
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:
>>> frompysat.solversimportMinisatGH>>> frompysat.examples.genhardimportPHP>>>>>> 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 callNone>>> m.delete()
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
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.
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:
>>> frompysat.solversimportCadical153>>> frompysat.examples.genhardimportParity>>>>>> 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 callNone>>> c.delete()
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.
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.
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:
>>> frompysat.solversimportMinisat22>>> 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()
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.
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:
>>> frompysat.solversimportMinisatGH>>> frompysat.examples.genhardimportPHP>>> fromthreadingimportTimer>>>>>> cnf=PHP(nof_holes=20)# PHP20 is too hard for a SAT solver>>> m=MinisatGH(bootstrap_with=cnf.clauses)>>>>>> definterrupt(s):>>> s.interrupt()>>>>>> timer=Timer(10,interrupt,[m])>>> timer.start()>>>>>> print(m.solve_limited(expect_interrupt=True))None>>> m.delete()
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.
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:
>>> frompysat.solversimportMinisatGH>>> frompysat.examples.genhardimportParity>>>>>> 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 callNone>>> m.delete()
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 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().
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).
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:
>>> frompysat.solversimportGlucose3>>>>>> 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()
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.)
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().
Parameters:
assumptions (iterable(int)) – a list of assumption literals.
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 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().
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 calli=0whilei<len(core):to_test=core[:i]+core[(i+1):]# doing a limited calliforacle.solve_limited(assumptions=to_test)==False:core=to_testelse:# True or *unknown*i+=1
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:
>>> defmodel_count(solver,formula,vlimit=None,warm_start=False):... withSolver(name=solver,bootstrap_with=formula,use_timer=True,warm_start=warm_start)asoracle:... count=0... whileoracle.solve()==True:... model=oracle.get_model()... ifvlimit:... model=model[:vlimit]... oracle.add_clause([-lforlinmodel])... 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
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).
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).
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.
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.