PB Encoder

The PB Encoder module provides access to a set of encoders that can be used to translate a Pseudo-Boolean (PB) or Cardinality (Card) constraint to CNF.

This module is divided into non-incremental encoders and incremental encoders and uses the PB encodings from PyPBLib and the Card encodings from PySAT.

Non-incremental encoders

class optilog.encoders.pb.Encoder

This class provides access to the most common Pseudo-Boolean and Cardinality constraint encodings implemented in PBLib.

All the methods in this class are static.

List of available constraint types for the Encoder class:

List of available Pseudo-Boolean encodings:

List of available Cardinality encodings:

static pb_encodings()

Returns a list of strings with all the available encodings for Pseudo-Boolean constraints.

>>> from optilog.encoders.pb import Encoder
>>> Encoder.pb_encodings()
['best', 'bdd', 'seqcounter', 'sortnetwork', 'adder', 'binarymerge']
Return type

List[str]

static card_encodings()

Returns a list of strings with all the available encodings for Cardinality constraints.

>>> from optilog.encoders.pb import Encoder
>>> Encoder.card_encodings()
['best', 'pairwise', 'seqcounter', 'sortnetwrk', 'cardnetwrk', 'bitwise', 'ladder', 'totalizer', 'mtotalizer', 'kmtotalizer']
Return type

List[str]

static get_incremental_pb_encodings()

Returns a list of strings with all the available incremental encodings for Pseudo-Boolean constraints.

>>> from optilog.encoders.pb import Encoder
>>> Encoder.get_incremental_pb_encodings()
['best', 'seqcounter', 'adder']
Return type

List[str]

static at_most_one(literals, weights=None, max_var=None, encoding='best')

Encodes the constraint \(\sum_{i=1}^{n} w_i l_i \leq 1\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals)).

  • encoding (str) – Encoding (see card_encodings() and pb_encodings()).

Return type

Tuple[int, List[List[int]]]

Returns

Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(x + 2y + z \leq 1\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.at_most_one(literals=[1,2,3], weights=[1,2,1])
(3, [[-2], [-3, -1]])

\(x + y + z \leq 1\) (Cardinality)

>>> Encoder.at_most_one(literals=[1,2,3])
(5, [[4, -1], [-2, 5], [-4, 5], [-2, -4], [-3, -5]])
static at_least_one(literals, weights=None, max_var=None, encoding='best')

Encodes the constraint \(\sum_{i=1}^{n} w_i l_i \geq 1\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals)).

  • encoding (str) – Encoding (see card_encodings() and pb_encodings()).

Return type

Tuple[int, List[List[int]]]

Returns

Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(x + 2y + z \geq 1\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.at_least_one([1,2,3], weights=[1,2,1])
(6, [[4], [1, 3, -5], [5, 2, -6], [6]])

\(x + y + z \geq 1\) (Cardinality)

>>> Encoder.at_least_one([1,2,3])
(3, [[1, 2, 3]])
static exactly_one(literals, weights=None, max_var=None, encoding='best')

Encodes the constraint \(\sum_{i=1}^{n} w_i l_i = 1\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals)).

  • encoding (str) – Encoding (see card_encodings() and pb_encodings()).

Return type

Tuple[int, List[List[int]]]

Returns

Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(2x + y + z = 1\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.exactly_one([1,2,3], weights=[2,1,1])
(3, [[-1], [3, 2], [-3, -2]])

\(x + y + z = 1\) (Cardinality)

>>> Encoder.exactly_one([1,2,3])
(5, [[1, 2, 3], [4, -1], [-2, 5], [-4, 5], [-2, -4], [-3, -5]])
static at_most_k(literals, bound, weights=None, max_var=None, encoding='best')

Encodes the constraint \(\sum_{i=1}^{n} w_i l_i \leq k\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • bound (int) – Upper bound of the constraint, using 1 is equivalent to call at_most_one()

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals)).

  • encoding (str) – Encoding (see card_encodings() and pb_encodings()).

Return type

Tuple[int, List[List[int]]]

Returns

Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(2x + y + z \leq 2\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.at_most_k([1,2,3], 2, weights=[2,1,1])
(9, [[4], [-4, 5], [-3, 5], [-4, -3, 6], [-2, 5], [-4, -2, 6], [-3, -2, 6], [-4, -3, -2, 7], [-1, 8], [-6, 8], [-1, -6, 9], [-9]])

\(x + y + z \leq 2\) (Cardinality)

>>> Encoder.at_most_k([1,2,3], 2)
(3, [[-1, -2, -3]])
static at_least_k(literals, bound, weights=None, max_var=None, encoding='best')

Encodes the constraint \(\sum_{i=1}^{n} w_i l_i \geq k\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • bound (int) – Upper bound of the constraint, using 1 is equivalent to call at_most_one()

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals)).

  • encoding (str) – Encoding (see card_encodings() and pb_encodings()).

Return type

Tuple[int, List[List[int]]]

Returns

Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(2x + y + z \geq 2\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.at_least_k([1,2,3], 2, weights=[2,1,1])
(9, [[4], [-4, 5], [3, 5], [-4, 3, 6], [2, 5], [-4, 2, 6], [3, 2, 6], [-4, 3, 2, 7], [1, 8], [-6, 8], [1, -6, 9], [-9]])

\(x + y + z \geq 2\) (Cardinality)

>>> Encoder.at_least_k([1,2,3], 2)
(5, [[4, 1], [2, 5], [-4, 5], [2, -4], [3, -5]])
static exactly_k(literals, bound, weights=None, max_var=None, encoding='best')

Encodes the constraint \(\sum_{i=1}^{n} w_i l_i = k\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • bound (int) – Upper bound of the constraint, using 1 is equivalent to call at_most_one()

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals)).

  • encoding (str) – Encoding (see card_encodings() and pb_encodings()).

Return type

Tuple[int, List[List[int]]]

Returns

Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(2x + y + z = 2\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.exactly_k([1,2,3], 2, weights=[2,1,1])
(8, [[4], [-5, -3], [-5, 3, -2], [-5, -2], [-6, 2], [-7, -3, 6], [-7, 3], [-7, 6], [-8, -1, 5], [-8, 1, 7], [-8, 5, 7], [8]])

\(x + y + z = 2\) (Cardinality)

>>> Encoder.exactly_k([1,2,3], 2)
(5, [[4, 1], [2, 5], [-4, 5], [2, -4], [3, -5], [-1, -2, -3]])
static range_k1_k2(literals, leqbound, geqbound, weights=None, max_var=None, encoding='best')

Encodes the constraint \(k2 \leq \sum_{i=1}^{n} w_i l_i \leq k1\) to CNF using the provided encoding.

Parameters
  • literals (List[int]) – List of literals (\(l_i\)).

  • weights (Optional[List[int]]) – List of weights (\(w_i\)).

  • leqbound (int) – The upper bound of the constraint, k1

  • geqbound (int) – The lower bound of the constraint, k2

:param : Maximum variable used so far (default: max(literals)). :type encoding: str :param encoding: Encoding (see card_encodings() and pb_encodings()). :rtype: Tuple[int, List[List[int]]] :return: Maximum DIMACS variable id used to encode the constraint and the list of SAT clauses encoding the constraint.

\(2 \leq 2x + y + z \leq 3\) (Pseudo-Boolean)

>>> from optilog.encoders.pb import Encoder
>>> Encoder.range_k1_k2([1,2,3], 3, 2, weights=[2,1,1])
(9, [[-3, -2, -1], [4], [-4, 5], [3, 5], [-4, 3, 6], [2, 5], [-4, 2, 6], [3, 2, 6], [-4, 3, 2, 7], [1, 8], [-6, 8], [1, -6, 9], [-9]])

\(1 \leq x + y + z \leq 2\) (Cardinality)

>>> Encoder.range_k1_k2([1,2,3], 2, 1)
(3, [[1, 2, 3], [-1, -2, -3]])

Incremental encoders

class optilog.encoders.pb.IncrementalEncoder(literals, bound=1, weights=None, max_var=None, encoding='best')

This class provides access to the most common incremental Pseudo-Boolean and Cardinality constraint encodings. The user can refine the bound once the constraint has been encoded. IncrementalEncoder only supports at most k constraints.

List of available Pseudo-Boolean encodings:

List of available Cardinality encodings:

Parameters
  • literals (List[int]) – List of literals

  • bound (int) – Bound of constraint (i.e. \(\leq bound\))

  • weights (Optional[List[int]]) – Weight of constraint (default None, unweighted)

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals))

  • encoding (str) – Encoding (see pb_encodings() and card_encodings()). Defaults to best

get_init_clauses()

Obtain the initial clauses that encode the constraint specified in the constructor of the class.

Return type

Tuple[int, List[List[int]]]

Returns

Returns the maximum auxiliary variable used so far and the list of clauses

>>> from optilog.encoders.pb import IncrementalEncoder
>>> enc = IncrementalEncoder([1,2,3], 3)
>>> enc.get_init_clauses()
(6, [[-3, 4], [-2, 4], [-3, -2, 5], [-1, 4], [-3, -1, 5], [-2, -1, 5], [-3, -2, -1, 6]])
static init(literals, bound=1, weights=None, max_var=None, encoding='best')

Utility method that returns an IncrementalEncoder instance and the result of calling get_init_clauses().

Parameters
  • literals (List[int]) – List of literals

  • bound (int) – Bound of constraint (i.e. ≤ bound)

  • weights (Optional[List[int]]) – Weight of constraint (default None, unweighted)

  • max_var (Optional[int]) – Maximum variable used so far (default: max(literals))

  • encoding (str) – Encoding (see pb_encodings() and card_encodings()). Defaults to best

Return type

Tuple[IncrementalEncoder, int, List[List[int]]]

Returns

IncrementalEncoder instance, maximum auxiliary variable used so far and list of clauses

>>> from optilog.encoders.pb import IncrementalEncoder
>>> IncrementalEncoder.init([1,2,3], 3)
(<IncrementalEncoder object>, 6, [[-3, 4], [-2, 4], [-3, -2, 5], [-1, 4], [-3, -1, 5], [-2, -1, 5], [-3, -2, -1, 6]])
extend(new_bound)

Refine the original constraint incrementally.

Warning

This method can only be used after calling the init() or get_init_clauses() methods.

Parameters

new_bound (int) – Refined bound

Return type

Tuple[int, List[List[int]]]

Returns

maximum auxiliary variable used so far and list of clauses that encode the refined constraint

>>> from optilog.encoders.pb import IncrementalEncoder
>>> enc, max_var, C = IncrementalEncoder.init([1,2,3], 3)
>>> enc.extend(2)
(6, [[-6]])
static pb_encodings()
Return type

List[str]

Returns

A list of strings with all the available encodings for Pseudo-Boolean constraints.

>>> from optilog.encoders.pb import IncrementalEncoder
>>> IncrementalEncoder.pb_encodings()
['best', 'seqcounter', 'adder']
static get_amo_encodings()
Return type

List[str]

Returns

A list of strings with all the available At Most One constraints.

>>> from optilog.encoders.pb import IncrementalEncoder
>>> IncrementalEncoder.get_amo_encodings()
['best', 'nested', 'bdd', 'bimander', 'commander', 'kproduct', 'binary', 'pairwise', 'totalizer']
static card_encodings()
Return type

List[str]

Returns

A list of strings with all the available encodings for Cardinality constraints.

>>> from optilog.encoders.pb import IncrementalEncoder
>>> IncrementalEncoder.card_encodings()
['best', 'bdd', 'card', 'totalizer']