Cardinality encodings (pysat.card
)#
List of classes#
This class represents a Clike 

This abstract class is responsible for the creation of cardinality constraints encoded to a CNF formula. 

This class implements the iterative totalizer encoding 11. 
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.
 1
Olivier Roussel, Vasco M. Manquinho. PseudoBoolean and Cardinality Constraints. Handbook of Satisfiability. 2009. pp. 695733
 2(1,2)
Steven David Prestwich. CNF Encodings. Handbook of Satisfiability. 2009. pp. 7597
 3
Carlos Ansótegui, Felip Manyà. Mapping Problems with FiniteDomain Variables to Problems with Boolean Variables. SAT (Selected Papers) 2004. pp. 115
 4
Ian P. Gent, Peter Nightingale. A New Encoding of Alldifferent Into SAT. In International workshop on modelling and reformulating constraint satisfaction problems 2004. pp. 95110
 5
Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. CP 2005. pp. 827831
 6
Kenneth E. Batcher. Sorting Networks and Their Applications. AFIPS Spring Joint Computing Conference 1968. pp. 307314
 7
Roberto Asin, Robert Nieuwenhuis, Albert Oliveras, Enric RodriguezCarbonell. Cardinality Networks and Their Applications. SAT 2009. pp. 167180
 8
Olivier Bailleux, Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. CP 2003. pp. 108122
 9
Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita. Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. ICTAI 2013. pp. 917
 10
António Morgado, Alexey Ignatiev, Joao MarquesSilva. MSCG: Robust CoreGuided MaxSAT Solving. System Description. JSAT 2015. vol. 9, pp. 129134
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. At this point only the iterative totalizer
11 encoding is supported. Iterative totalizer can be accessed with the
use of the ITotalizer
class.
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)
orCardEnc.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
, andencoding
. 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 betop_id+1
.Instead of
top_id
, one may want to use a pool of variable identifiersvpool
, which is automatically updated during the method call. In many circumstances, this is more convenient than usingtop_id
. Also note that parameterstop_id
andvpool
cannot be specified simultaneously.The default value of
encoding
isEnctype.seqcounter
.The method translates the AtLeast constraint into an AtMost constraint by negating the literals of
lits
, creating a new bound \(nk\) and invokingCardEnc.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()
andCardEnc.atmost()
. It shares the arguments and the return type with methodCardEnc.atleast()
. Please, see it for details.
 class pysat.card.EncType#
This class represents a Clike
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]
, wherelits
is a list of sizen
containing literals in the sum.
 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 classEncType
, 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 asself.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 asself.rhs
. A concrete bound \(k\) can be enforced by considering a unit clauseself.rhs[k]
. Note thatself.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 variablesself.cnf
andself.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 inself
.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 variableself.nof_new
.Also, if the upper bound is updated, a list of bounds
self.rhs
gets increased and its length becomesubound+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 inself
.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 variableself.nof_new
.Also, a list of bounds
self.rhs
gets increased and its length becomesubound+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 existingITotalizer
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 inself
.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 variableself.nof_new
.Also, if the upper bound is updated, a list of bounds
self.rhs
gets increased and its length becomesubound+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 fromself.__init__()
. Creates an object ofITotalizer
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 ofITotalizer
for details.