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:At most one:
Encoder.at_most_one()
At least one:
Encoder.at_least_one()
Exactly one:
Encoder.exactly_one()
At most k:
Encoder.at_most_k()
At least k:
Encoder.at_least_k()
Exactly k:
Encoder.exactly_k()
Range k1 - k2:
Encoder.range_k1_k2()
List of available Pseudo-Boolean encodings:
Adder networks [EenSorensson06]
Binary merge [MPS14]
BDD [EenSorensson06] [AbioNORodriguezC11]
Sequential weigh counters [HolldoblerMS12]
Sorting networks [EenSorensson06]
List of available Cardinality encodings:
bitwise [Pre09]
cardinality network [AsinNORodriguezC09]
ladder / regular [AnsoteguiM04]
pairwise [Pre09]
sequential counters [Sin05]
sorting networks [AsinNORodriguezC09]
totalizer [BB03]
totalizer modulo [OLH+13]
totalizer modulo for k-cardinality [MIMS14]
- 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 (seecard_encodings()
andpb_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 (seecard_encodings()
andpb_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 (seecard_encodings()
andpb_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 callat_most_one()
max_var (
Optional
[int
]) – Maximum variable used so far (default: max(literals)).encoding (
str
) – Encoding (seecard_encodings()
andpb_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 callat_most_one()
max_var (
Optional
[int
]) – Maximum variable used so far (default: max(literals)).encoding (
str
) – Encoding (seecard_encodings()
andpb_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 callat_most_one()
max_var (
Optional
[int
]) – Maximum variable used so far (default: max(literals)).encoding (
str
) – Encoding (seecard_encodings()
andpb_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, k1geqbound (
int
) – The lower bound of the constraint, k2
:param : Maximum variable used so far (default: max(literals)). :type encoding:
str
:param encoding: Encoding (seecard_encodings()
andpb_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:
Adder networks [EenSorensson06]
Sequential weigh counters [HolldoblerMS12]
List of available Cardinality encodings:
BDD [EenSorensson06] [AbioNORodriguezC11]
Cardinality network [AsinNORodriguezC09]
Totalizer [BB03]
- Parameters
literals (
List
[int
]) – List of literalsbound (
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 (seepb_encodings()
andcard_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 literalsbound (
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 (seepb_encodings()
andcard_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()
orget_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']