Pseudo-Boolean encodings (pysat.pb)#

List of classes#

EncType

This class represents a C-like enum type for choosing the pseudo-Boolean encoding to use.

PBEnc

Abstract class responsible for the creation of pseudo-Boolean 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 well-known 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 pseudo-Boolean 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\}\). Pseudo-Boolean constraints arise in a number of important practical applications. Thus, several encodings of pseudo-Boolean constraints into CNF formulas are known [2]. The list of pseudo-Boolean 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.

Module details#

class pysat.pb.EncType#

This class represents a C-like enum type for choosing the pseudo-Boolean 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 the bdd 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 pseudo-Boolean 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) or PBEnc.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), where l is an integer literal and w is an integer weight. The latter can be done only if no weights are specified separately. The type of encoding to use can be specified using the encoding parameter. By default, it is set to EncType.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:

pysat.formula.CNFPlus

previous

External engines (pysat.engines)

next

Formula processing (pysat.process)