7. Class Pb2cnf¶
The class Pb2cnf is the main interface to encode a PB constraint.
7.1. Constructor¶
Pb2cnf(config: PBConfig, stat: Statistics)
Creates a Pb2cnf with the specified configuration & statistics.
>>> from pypblib import pblib >>> conf = pblib.PBConfig() >>> stat = pblib.Statistics() >>> pb2 = pblib.Pb2cnf(conf, stat)
Pb2cnf(config: PBConfig)
Creates a Pb2cnf with the specified configuration.
>>> from pypblib import pblib >>> c = pblib.PBConfig() >>> c >>> pb2 = pblib.Pb2cnf(c)
Pb2cnf()
If the constructor does not receive any parameters, it will be created with default configuration.
>>> from pypblib import pblib >>> pb2 = pblib.Pb2cnf()
7.2. Methods sumary¶
| Return Type | Method |
|---|---|
| int | encode_at_most_k (literals: [int], k: long, formula: [], first_free_var: int) |
| int | encode_at_least_k (literals: [int], k: long, formula: [], first_free_var: int) |
| int | encode_leq (weights: [long], literals: [int], k: long, formula: [], first_free_var: int) |
| int | encode_geq (weights: [long], literals: [int], k: long, formula: [], first_free_var: int) |
| int | encode_both (weights: [long], literals [int], leq: long, geq: long, formula: [], first_free_var: int) |
| void |
|
| void |
|
7.3. Methods details¶
encode_at_most_k(literals: [int], k: long, formula: [], first_free_variable: int) → int¶For a simple interface ‘at most k’. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.
>>> from pypblib import pblib >>> literals = [1, 2, 3] >>> k = 1 >>> first_free_var = 4 >>> formula = [] >>> config = pblib.PBConfig() >>> max_var = pb2.encode_at_most_k(literals, k, formula, first_free_var) >>> print(max_var) 3 >>> print(formula) [[-3, -2], [-3, -1], [-2, -1]]
encode_at_least_k(literals: [int], k: long, formula: [], first_free_variable: int) → int¶For a simple interface ‘at least k’. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.
>>> from pypblib.pblib import PBConfig, Pb2cnf >>> formula = [] >>> pb2 = Pb2cnf(PBConfig()) >>> max_var = pb2.encode_at_least_k([1, 2, 3, 4], 2, formula, 5) >>>print(max_var) 10 >>> for clause in formula: ... for var in clause: ... print(var, end=" ") ... print("0") ... 5 0 1 -6 0 2 -6 0 1 2 -7 0 7 -8 0 6 3 -8 0 7 3 -9 0 9 -10 0 8 4 -10 0 10 0
encode_leq(weights: [long], literals: [int], k: long, formula: [], first_free_variable: int) → int¶For a simple interface and LEQ (less-equals) comparator. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.
>>> from pypblib.pblib import Pb2cnf, PBConfig >>> pb2 = Pb2cnf(PBConfig()) >>> formula = [] >>> weights = [2, 3, 1, 2] >>> literals = [1, 2, 3, 4] >>> first_free_var = 5 >>> leq = 3 >>> max_var = pb2.encode_leq(weights, literals, leq, formula, first_free_var) >>> print(max_var) 9 >>> print(formula) [[5], [-3, -6], [-1, -6], [6, -7], [-4, -7], [-1, -4, -8], [8, -9], [7, -2, -9], [9]]
encode_geq(weights: [long], literals: [int], k: long, formula: [], first_free_variable: int) → int¶For a simple interface and GEQ (greater-equals) comparator. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.
>>> from pypblib.pblib import Pb2cnf, PBConfig >>> pb2 = Pb2cnf(PBConfig()) >>> formula = [] >>> max_var = pb2.encode_geq([2, 1, 2, 4], [1, 2, 3, 4], 3, formula, 5) >>> print(max_var) 9 >>> print(formula) [[5], [2, -6], [1, -6], [2, 1, -7], [7, -8], [6, 3, -8], [8, 4, -9], [9]]
encode_both(weights: [long], literals [int], leq: long, geq: long, formula: [], first_free_variable: int) → int¶For a simple interface, LEQ (less-equals) and GEQ (greater-equals) comparators. The return value is the last used variable. Hence the next integer is the first free variable. At the end, the formula will contains the codification.
>>> from pypblib import pblib >>> config = pblib.PBConfig() >>> pb2 = pblib.Pb2cnf(config) >>> formula = [] >>> leq = 3 >>> geq = 1 >>> weights = [2, 3, 1, 1] >>> literals = [1, 2, 3, 4] >>> first_free_var = 5 >>> max_var = pb2.encode_both(weights, literals, leq, geq, formula, first_free_var) >>> print(max_var) 10 >>> for clause in formula: ... for var in clause: ... print(var, end=" ") ... print("0") ... 4 3 2 1 0 5 0 -3 -6 0 -4 -6 0 6 -7 0 -1 -7 0 -3 -4 -8 0 8 -1 -9 0 9 -10 0 7 -2 -10 0 10 0
encode(constr: PBConstraint, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)¶For this sophisticated interface you should use, besides the PBConstraint, a VectorClauseDatabase and a AuxVarManager to encode a pseudo boolean constriant. At the end, the formula will contains the codification.
>>> from pypblib import pblib >>> wl_List = [pblib.WeightedLit(1,3), pblib.WeightedLit(2,1), pblib.WeightedLit(3,5)] >>> comparator = pblib.GEQ >>> bound = 1 >>> aux_var = pblib.AuxVarManager(4) >>> constr = pblib.PBConstraint(wl_List, comparator, bound) >>> config = pblib.PBConfig() >>> formula = pblib.VectorClauseDatabase(config) >>> pb2cnf = pblib.Pb2cnf(config) >>> pb2cnf.encode(constr, formula, aux_var) >>> print(formula) 4 0 2 1 -5 0 5 3 -6 0 6 0 >>> formula.print_formula("encode_test.cnf", aux_var.get_biggest_returned_auxvar())
encode_inc_initial(inc_constr: IncPBConstraint, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)¶For incremental pseudo boolean constraint. You should use, besides the IncPBConstraint, a VectorClauseDatabase and a AuxVarManager to encode. At the end, the formula will contains the codification.
>>> from pypblib import pblib >>> wl1 = pblib.WeightedLit(1, 2) >>> wl2 = pblib.WeightedLit(2, 2) >>> wl3 = pblib.WeightedLit(3, -1) >>> i_contr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 3) >>> aux_var = pblib.AuxVarManager(4) >>> config = pblib.PBConfig() >>> formula = pblib.VectorClauseDatabase(config) >>> pb2 = pblib.Pb2cnf() >>> pb2.encode_inc_initial(i_contr, formula, aux_var)