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 Pindakaas package is installed, e.g. from PyPI:

$ pip install python-sat[pb]

This module provides access to the pseudo-Boolean encodings of the Pindakaas library [1], a Rust library for encoding pseudo-Boolean and integer constraints into CNF. Pindakaas has a number of additional features (e.g. integer variables and further encodings) that are not accessible through this module. If a user needs any of them, Pindakaas can be used as a standalone library alongside PySAT.

[1]

Hendrik Bierlee, Jip J. Dekker. Pindakaas. Software. https://doi.org/10.5281/zenodo.10851855

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], binary merge [6], the watchdog encoding [7], the generalized totalizer [8], and the mixed radix encoding [9]. Access to all cardinality encodings can be made through the main class of this module, which is PBEnc.

[2]

Olivier Roussel, Vasco M. Manquinho. Pseudo-Boolean and Cardinality Constraints. Handbook of Satisfiability. 2009. pp. 695-733

[3] (1,2,3)

Niklas Eén, Niklas Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT. vol. 2(1-4). 2006. pp. 1-26

[4]

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. BDDs for Pseudo-Boolean Constraints - Revisited. SAT. 2011. pp. 61-75

[5]

Steffen Hölldobler, Norbert Manthey, Peter Steinke. A Compact Encoding of Pseudo-Boolean Constraints into SAT. KI. 2012. pp. 107-118

[6]

Norbert Manthey, Tobias Philipp, Peter Steinke. A More Compact Translation of Pseudo-Boolean Constraints into CNF Such That Generalized Arc Consistency Is Maintained. KI. 2014. pp. 123-134

[7]

Olivier Bailleux, Yacine Boufkhad, Olivier Roussel. New Encodings of Pseudo-Boolean Constraints into CNF. SAT 2009. pp. 181-194

[8]

Saurabh Joshi, Ruben Martins, Vasco Manquinho. Generalized Totalizer Encoding for Pseudo-Boolean Constraints. CP 2015. pp. 200-209

[9]

Anpeng Zha, Miyuki Koshimura, Hiroshi Fujita. N-level Modulo-based CNF Encodings of Pseudo-Boolean Constraints for MaxSAT. Constraints 24(2). 2019. pp. 133-161

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
watchdog   = 7
totalizer  = 8
mixedradix = 9

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 Pindakaas uses its default encoder for the shape of the constraint (e.g. the totalizer for PB and cardinality constraints). Any other encoding is applied to every shape of constraint, including cardinality and AtMostOne constraints. Finally, binmerge is the watchdog encoding of Pindakaas, counting with sorting networks rather than totalizers.

exception pysat.pb.NoSuchEncodingError

This exception is raised when creating an unknown LEQ, GEQ, or Equals constraint encoding.

add_note(note, /)

Add a note to the 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)
[[-5, 4], [-6, 5], [-2, 5], [-1, 4], [-1, -2, 6], [-4, -3]]
>>> cnf = PBEnc.equals(lits=[1, 2, 3], weights=[1, 2, 3], bound=3, encoding=EncType.bdd)
>>> print(cnf.clauses)
[[-1, 5], [1, -5], [-2, 4], [-5, 4], [2, -4], [5, -4], [-4, -3], [4, 3]]

classmethod atleast(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0, conditionals=None)

A synonym for PBEnc.geq().

classmethod atmost(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0, conditionals=None)

A synonym for PBEnc.leq().

classmethod equals(lits, weights=None, bound=1, top_id=None, vpool=None, encoding=0, conditionals=None)

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, conditionals=None)

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, conditionals=None)

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.CNFPlus.

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 Pindakaas to choose the encoding type.

The final optional argument is conditionals, where a list of literals can be passed to be used as the antecedent for the PB constraint, which makes it “reified”. If the argument is set to None, the constraint won’t be reified.

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.

• conditionals (list(int) or None) – a list of variables that imply this constraint.

Return type:

pysat.formula.CNFPlus