PseudoBoolean encodings (pysat.pb
)#
List of classes#
This class represents a Clike 

Abstract class responsible for the creation of pseudoBoolean constraints encoded to a CNF formula. 
Module description#
Note
Functionality of this module is available only if the PyPBLib package is installed, e.g. from PyPI:
$ pip install pypblib
This module provides access to the basic functionality of the PyPBLib
library developed by the Logic
Optimization Group of the University of Lleida.
PyPBLib provides a user with an extensive Python API to the wellknown
PBLib library
[1]. Note the PyPBLib has a number of additional features that cannot
be accessed through PySAT at this point. (One concrete example is a
range of cardinality encodings, which clash with the internal
pysat.card
module.) If a user needs some functionality of PyPBLib
missing in this module, he/she may apply PyPBLib as a standalone library,
when working with PySAT.
A pseudoBoolean constraint is a constraint of the form:
\(\left(\sum_{i=1}^n{a_i\cdot x_i}\right)\circ k\), where
\(a_i\in\mathbb{N}\), \(x_i\in\{y_i,\neg{y_i}\}\),
\(y_i\in\mathbb{B}\), and \(\circ\in\{\leq,=,\geq\}\).
PseudoBoolean constraints arise in a number of important practical
applications. Thus, several encodings of pseudoBoolean constraints into
CNF formulas are known [2]. The list of pseudoBoolean encodings
supported by this module include BDD [3] [4], sequential weight counters
[5], sorting networks [3], adder networks [3], and binary merge [6].
Access to all cardinality encodings can be made through the main class of
this module, which is PBEnc
.
Olivier Roussel, Vasco M. Manquinho. PseudoBoolean and Cardinality Constraints. Handbook of Satisfiability. 2009. pp. 695733
Niklas Eén, Niklas Sörensson. Translating PseudoBoolean Constraints into SAT. JSAT. vol. 2(14). 2006. pp. 126
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric RodríguezCarbonell. BDDs for PseudoBoolean Constraints  Revisited. SAT. 2011. pp. 6175
Steffen Hölldobler, Norbert Manthey, Peter Steinke. A Compact Encoding of PseudoBoolean Constraints into SAT. KI. 2012. pp. 107118
Norbert Manthey, Tobias Philipp, Peter Steinke. A More Compact Translation of PseudoBoolean Constraints into CNF Such That Generalized Arc Consistency Is Maintained. KI. 2014. pp. 123134
Module details#
 class pysat.pb.EncType#
This class represents a Clike
enum
type for choosing the pseudoBoolean encoding to use. The values denoting the encodings are:best = 0 bdd = 1 seqcounter = 2 sortnetwrk = 3 adder = 4 binmerge = 5 native = 6
The desired encoding can be selected either directly by its integer identifier, e.g.
2
, or by its alphabetical name, e.g.EncType.seqcounter
.All the encodings are produced and returned as a list of clauses in the
pysat.formula.CNFPlus
format.Note that the encoding type can be set to
best
, in which case the encoder selects one of the other encodings from the list (in most cases, this invokes thebdd
encoder).
 exception pysat.pb.NoSuchEncodingError#
This exception is raised when creating an unknown LEQ, GEQ, or Equals constraint encoding.
 with_traceback()#
Exception.with_traceback(tb) – set self.__traceback__ to tb and return self.
 class pysat.pb.PBEnc#
Abstract class responsible for the creation of pseudoBoolean constraints encoded to a CNF formula. The class has three main class methods for creating LEQ, GEQ, and Equals constraints. Given (1) either a list of weighted literals or a list of unweighted literals followed by a list of weights, (2) an integer bound and an encoding type, each of these methods returns an object of class
pysat.formula.CNFPlus
representing the resulting CNF formula.Since the class is abstract, there is no need to create an object of it. Instead, the methods should be called directly as class methods, e.g.
PBEnc.atmost(wlits, bound)
orPBEnc.equals(lits, weights, bound)
. An example usage is the following:>>> from pysat.pb import * >>> cnf = PBEnc.atmost(lits=[1, 2, 3], weights=[1, 2, 3], bound=3) >>> print(cnf.clauses) [[4], [1, 5], [2, 5], [5, 3, 6], [6]] >>> cnf = PBEnc.equals(lits=[1, 2, 3], weights=[1, 2, 3], bound=3, encoding=EncType.bdd) >>> print(cnf.clauses) [[4], [5, 2], [5, 2, 1], [5, 1], [6, 1], [7, 2, 6], [7, 2], [7, 6], [8, 3, 5], [8, 3, 7], [8, 5, 7], [8]]
 classmethod atleast(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0)#
A synonym for
PBEnc.geq()
.
 classmethod atmost(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0)#
A synonim for
PBEnc.leq()
.
 classmethod equals(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0)#
This method can be used for creating a CNF encoding of a weighted EqualsK constraint, i.e. of \(\sum_{i=1}^{n}{a_i\cdot x_i}= k\). The method shares the arguments and the return type with method
PBEnc.leq()
. Please, see it for details.
 classmethod geq(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0)#
This method can be used for creating a CNF encoding of a GEQ (weighted AtLeastK) constraint, i.e. of \(\sum_{i=1}^{n}{a_i\cdot x_i}\geq k\). The method shares the arguments and the return type with method
PBEnc.leq()
. Please, see it for details.
 classmethod leq(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0)#
This method can be used for creating a CNF encoding of a LEQ (weighted AtMostK) constraint, i.e. of \(\sum_{i=1}^{n}{a_i\cdot x_i}\leq k\). The resulting set of clauses is returned as an object of class
formula.CNF
.The input list of literals can contain either integers or pairs
(l, w)
, wherel
is an integer literal andw
is an integer weight. The latter can be done only if noweights
are specified separately. The type of encoding to use can be specified using theencoding
parameter. By default, it is set toEncType.best
, i.e. it is up to the PBLib encoder to choose the encoding type. Parameters:
lits (iterable(int)) – a list of literals in the sum.
weights (iterable(int)) – a list of weights
bound (int) – the value of bound \(k\).
top_id (integer or None) – top variable identifier used so far.
vpool (
IDPool
) – variable pool for counting the number of variables.encoding (integer) – identifier of the encoding to use.
 Return type: