Cardinality encodings (`pysat.card`)#

List of classes#

`EncType`	This class represents a C-like `enum` type for choosing the cardinality encoding to use.
`CardEnc`	This abstract class is responsible for the creation of cardinality constraints encoded to a CNF formula.
`ITotalizer`	This class implements the iterative totalizer encoding [11].
`ISeqCounter`	This class implements an iterative sequential-counter encoding.

Module description#

This module provides access to various cardinality constraint [1] encodings to formulas in conjunctive normal form (CNF). These include pairwise [2], bitwise [2], ladder/regular [3] [4], sequential counters [5], sorting [6] and cardinality networks [7], totalizer [8], modulo totalizer [9], and modulo totalizer for \(k\)-cardinality [10], as well as a native cardinality constraint representation supported by the MiniCard solver.

A cardinality constraint is a constraint of the form: \(\sum_{i=1}^n{x_i}\leq k\). Cardinality constraints are ubiquitous in practical problem formulations. Note that the implementation of the pairwise, bitwise, and ladder encodings can only deal with AtMost1 constraints, e.g. \(\sum_{i=1}^n{x_i}\leq 1\).

Access to all cardinality encodings can be made through the main class of this module, which is CardEnc.

Additionally, to the standard cardinality encodings that are basically “static” CNF formulas, the module is designed to able to construct incremental cardinality encodings, i.e. those that can be incrementally extended at a later stage. The iterative totalizer [11] is available through ITotalizer. An iterative sequential counter is available through ISeqCounter; it supports increasing the bound and obtaining constraint literals for prefixes of the input.

Module details#

class pysat.card.CardEnc#

This abstract class is responsible for the creation of cardinality constraints encoded to a CNF formula. The class has three class methods for creating AtMostK, AtLeastK, and EqualsK constraints. Given a list of literals, 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. CardEnc.atmost(lits, bound) or CardEnc.equals(lits, bound). An example usage is the following:

>>> from pysat.card import *
>>> cnf = CardEnc.atmost(lits=[1, 2, 3], encoding=EncType.pairwise)
>>> print(cnf.clauses)
[[-1, -2], [-1, -3], [-2, -3]]
>>> cnf = CardEnc.equals(lits=[1, 2, 3], encoding=EncType.pairwise)
>>> print(cnf.clauses)
[[1, 2, 3], [-1, -2], [-1, -3], [-2, -3]]

classmethod atleast(lits, bound=1, top_id=None, vpool=None, encoding=1)#

This method can be used for creating a CNF encoding of an AtLeastK constraint, i.e. of \(\sum_{i=1}^{n}{x_i}\geq k\). The method takes 1 mandatory argument lits and 3 default arguments can be specified: bound, top_id, vpool, and encoding.

Parameters:

lits (iterable(int)) – a list of literals in the sum.
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.

Parameter top_id serves to increase integer identifiers of auxiliary variables introduced during the encoding process. This is helpful when augmenting an existing CNF formula with the new cardinality encoding to make sure there is no collision between identifiers of the variables. If specified, the identifiers of the first auxiliary variable will be top_id+1.

Instead of top_id, one may want to use a pool of variable identifiers vpool, which is automatically updated during the method call. In many circumstances, this is more convenient than using top_id. Also note that parameters top_id and vpool cannot be specified simultaneously.

The default value of encoding is EncType.seqcounter.

The method translates the AtLeast constraint into an AtMost constraint by negating the literals of lits, creating a new bound \(n-k\) and invoking CardEnc.atmost() with the modified list of literals and the new bound.

Raises:

CardEnc.NoSuchEncodingError – if encoding does not exist.
ValueError – if bound is meaningless for encoding.

Return type:

a CNFPlus object where the new clauses (or the new native atmost constraint) are stored.

classmethod atmost(lits, bound=1, top_id=None, vpool=None, encoding=1)#: This method can be used for creating a CNF encoding of an AtMostK constraint, i.e. of \(\sum_{i=1}^{n}{x_i}\leq k\). The method shares the arguments and the return type with method CardEnc.atleast(). Please, see it for details.

classmethod equals(lits, bound=1, top_id=None, vpool=None, encoding=1)#: This method can be used for creating a CNF encoding of an EqualsK constraint, i.e. of \(\sum_{i=1}^{n}{x_i}= k\). The method makes consecutive calls of both CardEnc.atleast() and CardEnc.atmost(). It shares the arguments and the return type with method CardEnc.atleast(). Please, see it for details.

class pysat.card.EncType#

This class represents a C-like enum type for choosing the cardinality encoding to use. The values denoting the encodings are:

pairwise    = 0
seqcounter  = 1
sortnetwrk  = 2
cardnetwrk  = 3
bitwise     = 4
ladder      = 5
totalizer   = 6
mtotalizer  = 7
kmtotalizer = 8
native      = 9

The desired encoding can be selected either directly by its integer identifier, e.g. 2, or by its alphabetical name, e.g. EncType.sortnetwrk.

Note that while most of the encodings are produced as a list of clauses, the “native” encoding of MiniCard is managed as one clause. Given an AtMostK constraint \(\sum_{i=1}^n{x_i\leq k}\), the native encoding represents it as a pair [lits, k], where lits is a list of size n containing literals in the sum.

class pysat.card.ISeqCounter(lits=[], ubound=1, top_id=None)#

This class implements an iterative sequential-counter encoding. Like ITotalizer, this class is not abstract and its objects once created can be reused several times: the bound can be increased, and the internal state can be read out as standalone constraint literals via get_constraint(). The interface intentionally mirrors ITotalizer’s.

The constructor of the class object takes 3 default arguments.

Parameters:

lits (iterable(int)) – a list of literals to sum.
ubound (int) – the largest potential bound to use.
top_id (integer or None) – top variable identifier used so far.

The encoding of the current counter can be accessed with the use of CNF variable stored as self.cnf. Potential bounds are not imposed by default but can be added as unit clauses in the final CNF formula. The bounds are stored in the list of Boolean variables as self.rhs. A concrete bound \(k\) can be enforced by considering a unit clause -self.rhs[k]. Note that -self.rhs[0] enforces all literals of the sum to be false.

An ISeqCounter object should be deleted if it is not needed anymore.

Possible usage of the class is shown below:

>>> from pysat.card import ISeqCounter
>>> t = ISeqCounter(lits=[1, 2, 3], ubound=1)
>>> print(t.cnf.clauses)
[[-1, 4], [-4, 5], [-2, 5], [-5, 6], [-3, 6], [-4, -2, 7], [-7, 8], [-5, -3, 8]]
>>> print(t.rhs)
[6, 8]
>>> t.delete()

delete()#: Destroys a previously constructed ISeqCounter object. Internal variables self.cnf and self.rhs get cleaned.

get_constraint(prefix_len, bound)#

Get the literal whose negation requires that the sum of the first prefix_len literals of self.lits is at most bound. This lets a caller reuse the internal state of a partially-built counter as a standalone constraint, rather than only ever asserting the counter’s own top-level bound in self.rhs.

Parameters:

prefix_len (int) – length of the prefix of self.lits to sum.
bound (int) – an upper bound already covered by the counter, i.e. bound < len(self.rhs).

Returns:

the requested literal, or None if prefix_len and bound do not satisfy 0 <= bound < len(self.rhs) and bound < prefix_len <= len(self.lits).

Return type:

int or None

increase(ubound=1, top_id=None)#

Increases a potential upper bound that can be imposed on the literals in the sum of an existing ISeqCounter object to a new value.

Parameters:

ubound (int) – a new upper bound.
top_id (integer or None) – a new top variable identifier.

The top identifier top_id applied only if it is greater than the one used in self.

This method creates additional clauses encoding the existing counter up to the new upper bound given and appends them to the list of clauses of CNF self.cnf. The number of newly created clauses is stored in variable self.nof_new.

Also, a list of bounds self.rhs gets increased and its length becomes ubound+1.

The method can be used in the following way:

>>> from pysat.card import ISeqCounter
>>> t = ISeqCounter(lits=[1, 2, 3], ubound=1)
>>> print(t.cnf.clauses)
[[-1, 4], [-4, 5], [-2, 5], [-5, 6], [-3, 6], [-4, -2, 7], [-7, 8], [-5, -3, 8]]
>>> print(t.rhs)
[6, 8]
>>>
>>> t.increase(ubound=2)
>>> print(t.cnf.clauses)
[[-1, 4], [-4, 5], [-2, 5], [-5, 6], [-3, 6], [-4, -2, 7], [-7, 8], [-5, -3, 8], [-7, -3, 9]]
>>> print(t.cnf.clauses[-t.nof_new:])
[[-7, -3, 9]]
>>> print(t.rhs)
[6, 8, 9]
>>> t.delete()

new(lits=[], ubound=1, top_id=None)#: The actual constructor of ISeqCounter. Invoked from self.__init__(). Creates an object of ISeqCounter given a list of literals in the sum, the largest potential bound to consider, as well as the top variable identifier used so far. See the description of ISeqCounter for details.

class pysat.card.ITotalizer(lits=[], ubound=1, top_id=None)#

This class implements the iterative totalizer encoding [11]. Note that ITotalizer can be used only for creating AtMostK constraints. In contrast to class EncType, this class is not abstract and its objects once created can be reused several times. The idea is that a totalizer tree can be extended, or the bound can be increased, as well as two totalizer trees can be merged into one.

The constructor of the class object takes 3 default arguments.

Parameters:

lits (iterable(int)) – a list of literals to sum.
ubound (int) – the largest potential bound to use.
top_id (integer or None) – top variable identifier used so far.

The encoding of the current tree can be accessed with the use of CNF variable stored as self.cnf. Potential bounds are not imposed by default but can be added as unit clauses in the final CNF formula. The bounds are stored in the list of Boolean variables as self.rhs. A concrete bound \(k\) can be enforced by considering a unit clause -self.rhs[k]. Note that -self.rhs[0] enforces all literals of the sum to be false.

An ITotalizer object should be deleted if it is not needed anymore.

Possible usage of the class is shown below:

>>> from pysat.card import ITotalizer
>>> t = ITotalizer(lits=[1, 2, 3], ubound=1)
>>> print(t.cnf.clauses)
[[-2, 4], [-1, 4], [-1, -2, 5], [-4, 6], [-5, 7], [-3, 6], [-3, -4, 7]]
>>> print(t.rhs)
[6, 7]
>>> t.delete()

Alternatively, an object can be created using the with keyword. In this case, the object is deleted automatically:

>>> from pysat.card import ITotalizer
>>> with ITotalizer(lits=[1, 2, 3], ubound=1) as t:
...     print(t.cnf.clauses)
[[-2, 4], [-1, 4], [-1, -2, 5], [-4, 6], [-5, 7], [-3, 6], [-3, -4, 7]]
...     print(t.rhs)
[6, 7]

delete()#: Destroys a previously constructed ITotalizer object. Internal variables self.cnf and self.rhs get cleaned.

extend(lits=[], ubound=None, top_id=None)#

Extends the list of literals in the sum and (if needed) increases a potential upper bound that can be imposed on the complete list of literals in the sum of an existing ITotalizer object to a new value.

Parameters:

lits (iterable(int)) – additional literals to be included in the sum.
ubound (int) – a new upper bound.
top_id (integer or None) – a new top variable identifier.

The top identifier top_id applied only if it is greater than the one used in self.

This method creates additional clauses encoding the existing totalizer tree augmented with new literals in the sum and updating the upper bound. As a result, it appends the new clauses to the list of clauses of CNF self.cnf. The number of newly created clauses is stored in variable self.nof_new.

Also, if the upper bound is updated, a list of bounds self.rhs gets increased and its length becomes ubound+1. Otherwise, it is updated with new values.

The method can be used in the following way:

>>> from pysat.card import ITotalizer
>>> t = ITotalizer(lits=[1, 2], ubound=1)
>>> print(t.cnf.clauses)
[[-2, 3], [-1, 3], [-1, -2, 4]]
>>> print(t.rhs)
[3, 4]
>>>
>>> t.extend(lits=[5], ubound=2)
>>> print(t.cnf.clauses)
[[-2, 3], [-1, 3], [-1, -2, 4], [-5, 6], [-3, 6], [-4, 7], [-3, -5, 7], [-4, -5, 8]]
>>> print(t.cnf.clauses[-t.nof_new:])
[[-5, 6], [-3, 6], [-4, 7], [-3, -5, 7], [-4, -5, 8]]
>>> print(t.rhs)
[6, 7, 8]
>>> t.delete()

increase(ubound=1, top_id=None)#

Increases a potential upper bound that can be imposed on the literals in the sum of an existing ITotalizer object to a new value.

Parameters:

ubound (int) – a new upper bound.
top_id (integer or None) – a new top variable identifier.

The top identifier top_id applied only if it is greater than the one used in self.

This method creates additional clauses encoding the existing totalizer tree up to the new upper bound given and appends them to the list of clauses of CNF self.cnf. The number of newly created clauses is stored in variable self.nof_new.

Also, a list of bounds self.rhs gets increased and its length becomes ubound+1.

The method can be used in the following way:

>>> from pysat.card import ITotalizer
>>> t = ITotalizer(lits=[1, 2, 3], ubound=1)
>>> print(t.cnf.clauses)
[[-2, 4], [-1, 4], [-1, -2, 5], [-4, 6], [-5, 7], [-3, 6], [-3, -4, 7]]
>>> print(t.rhs)
[6, 7]
>>>
>>> t.increase(ubound=2)
>>> print(t.cnf.clauses)
[[-2, 4], [-1, 4], [-1, -2, 5], [-4, 6], [-5, 7], [-3, 6], [-3, -4, 7], [-3, -5, 8]]
>>> print(t.cnf.clauses[-t.nof_new:])
[[-3, -5, 8]]
>>> print(t.rhs)
[6, 7, 8]
>>> t.delete()

merge_with(another, ubound=None, top_id=None)#

This method merges a tree of the current ITotalizer object, with a tree of another object and (if needed) increases a potential upper bound that can be imposed on the complete list of literals in the sum of an existing ITotalizer object to a new value.

Parameters:

another (ITotalizer) – another totalizer to merge with.
ubound (int) – a new upper bound.
top_id (integer or None) – a new top variable identifier.

The top identifier top_id applied only if it is greater than the one used in self.

This method creates additional clauses encoding the existing totalizer tree merged with another totalizer tree into one sum and updating the upper bound. As a result, it appends the new clauses to the list of clauses of CNF self.cnf. The number of newly created clauses is stored in variable self.nof_new.

Also, if the upper bound is updated, a list of bounds self.rhs gets increased and its length becomes ubound+1. Otherwise, it is updated with new values.

The method can be used in the following way:

>>> from pysat.card import ITotalizer
>>> with ITotalizer(lits=[1, 2], ubound=1) as t1:
...     print(t1.cnf.clauses)
[[-2, 3], [-1, 3], [-1, -2, 4]]
...     print(t1.rhs)
[3, 4]
...
...     t2 = ITotalizer(lits=[5, 6], ubound=1)
...     print(t1.cnf.clauses)
[[-6, 7], [-5, 7], [-5, -6, 8]]
...     print(t1.rhs)
[7, 8]
...
...     t1.merge_with(t2)
...     print(t1.cnf.clauses)
[[-2, 3], [-1, 3], [-1, -2, 4], [-6, 7], [-5, 7], [-5, -6, 8], [-7, 9], [-8, 10], [-3, 9], [-4, 10], [-3, -7, 10]]
...     print(t1.cnf.clauses[-t1.nof_new:])
[[-6, 7], [-5, 7], [-5, -6, 8], [-7, 9], [-8, 10], [-3, 9], [-4, 10], [-3, -7, 10]]
...     print(t1.rhs)
[9, 10]
...
...     t2.delete()

new(lits=[], ubound=1, top_id=None)#: The actual constructor of ITotalizer. Invoked from self.__init__(). Creates an object of ITotalizer given a list of literals in the sum, the largest potential bound to consider, as well as the top variable identifier used so far. See the description of ITotalizer for details.

exception pysat.card.NoSuchEncodingError#

This exception is raised when creating an unknown an AtMostK, AtLeastK, or EqualK constraint encoding.

add_note(note, /)#: Add a note to the exception

with_traceback(tb, /)#: Set self.__traceback__ to tb and return self.

exception pysat.card.UnsupportedBound#

This exception is raised when creating a pairwise, or bitwise, or ladder encoding of AtMostK, AtLeastK, or EqualsK with the bound different from 1 and N - 1.

add_note(note, /)#: Add a note to the exception

with_traceback(tb, /)#: Set self.__traceback__ to tb and return self.

Cardinality encodings (pysat.card)#

List of classes#

Module description#

Module details#

Cardinality encodings (`pysat.card`)#