Pypb.Pblib - Constants¶
Comparators constants¶
Comparator can be less-equal, greater-equal or a combination of both.
-
pypblib.pblib.GEQ¶
-
pypblib.pblib.LEQ¶
-
pypblib.pblib.BOTH¶
Configuration constants¶
PB Encoder¶
-
pypblib.pblib.PB_BEST¶
-
pypblib.pblib.PB_BDD¶ Binary Desition Diagrams. BDD-based encodings have important advantages, such as sharing the same BDD for representing many constraints. Requieres additional variables. Exponential.
-
pypblib.pblib.PB_SWC¶ Sequential Weight Counter. SWC encoding is a modification of the sequential counter (SEQ) encoding, which translates cardinality constraints into SAT. Similar to BDD but useful for incremental encoding.
-
pypblib.pblib.PB_SORTINGNETWORKS¶ A (Boolean) sorting network is a circuit that receives n Boolean inputs x1,…,xn, and permutes them to obtain the sorted outputs y1,…,yn.
-
pypblib.pblib.PB_ADDER¶ Linear inequalities can be encoded into CNF in linear time and space, and uses adders as the basic operator. Requieres additional varialbes. Polynomial.
-
pypblib.pblib.PB_BINARY_MERGE¶ The Binary Merger encoding requires O(n^2 log^2(n) log(w[max])) clauses. If GAC should not be maintained, our encoding requires only O(n log^2(n) log(w[max])).