3. Class IncPBConstraint

3.1. Constructor

IncPBConstraint(weightedlits: [WeightedLits], comparator, bound: int)

Creates an object to represents a Pseudo-Boolean incremental costraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2,-1)
>>> wl3 = pblib.WeightedLit(3, 3)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.LEQ, 3)
>>> i_constr
+2x1-1x2+3x3<=3

IncPBConstraint(weightedlits: [WeightedLits], comparator, bound_geq: int, bound_leq: int)

Creates an object to represents a Pseudo-Boolean incremental costraint, in case pblib.BOTH comparator and bound less-equals and greater-equal are different.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2,-1)
>>> wl3 = pblib.WeightedLit(3, 3)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.BOTH, 3, -1)
>>> i_constr
-1<=+2x1-1x2+3x3<=3

3.3. Methods details

add_conditional(cond: int)

Adds a conditional to the incremental constraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1,-3)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> wl3 = pblib.WeightedLit(3, 2)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.LEQ, 1)
>>> i_constr
-3x1+x2+2x3<=1
>>> i_constr.add_conditional(3)
add_conditionals(conds: [int])

Adds a list of conditionals to the incremental constraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1,-3)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> wl3 = pblib.WeightedLit(2, 2)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.LEQ, 1)
>>> i_constr.add_conditionals([2, 3])
get_conditionals() → [int]

Returns a list of incremental conditionals.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 3)
>>> wl3 = pblib.WeightedLit(3, -1)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.LEQ, 2)
>>> i_constr.add_conditionals([1, 3])
>>> i_constr.get_conditionals()
[1, 3]
clear_conditionals()

Removes all conditionals in a incremental constraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 3)
>>> wl3 = pblib.WeightedLit(3, -1)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.LEQ, 2)
>>> i_constr.add_conditionals([1, 3])
>>> i_constr.get_conditionals()
[1, 3]
>>> i_constr.clear_conditionals()
>>> cond = i_constr.get_conditionals()
[]
get_comparator() → comparator

Returns an int to represents the comparator (GEQ = 0, LEQ = 1 and BOTH = 2).

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 1)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2],
                                  pblib.GEQ, 1)
>>> comp = i_constr.get_comparator()
>>> print(comp)
0
get_leq() → long

Returns the less-equal value bound of the incremental constraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 1)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> i_constr = pblib.PBConstraint([wl1, wl2],
                              pblib.LEQ, 1)
>>> n = i_constr.get_leq()
>>> print(n)
1
get_geq() → long

Returns the greater-equal value bound of the incremental constraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 1)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> i_constr = pblib.PBConstraint([wl1, wl2],
                              pblib.GEQ, 0)
>>> n = i_constr.get_geq()
>>> print(n)
0
set_comparator(comparator)

Sets the incremental constraint’s comparator to specified value.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 1)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> wl3 = pblib.WeightedLit(3, -1)
>>> wls = [wl1, wl2, wl3]
>>> i_constr = pblib.IncPBConstraint(wls,
                              pblib.LEQ, 4)
>>> print(i_constr.get_comparator())
1
>>> i_constr.set_comparator(pblib.GEQ)
>>> print(i_constr.get_comparator())
0
encode_new_geq(geq_bound: long, VectorClauseDatabase: formula, AuxVarManager: aux_var)

After the initial encoding of an incremental pseudo-boolean constraint, it is possible to encode a new (tighter) bounds with this method. Encodes an incremental constraint with a new greater-equal bound.

Example:

#!/usr/bin/env python3
# -*- coding: utf-8 -*-

from pypblib import pblib

#
###############################################################################

def test_formula():
    wl1 = pblib.WeightedLit(1, 1)
    wl2 = pblib.WeightedLit(2, 1)
    wl3 = pblib.WeightedLit(3, 1)
    wl4 = pblib.WeightedLit(4, -1)
    wl5 = pblib.WeightedLit(5, -1)
    wls = [wl1, wl2, wl3, wl4, wl5]
    config = pblib.PBConfig()
    aux_var = pblib.AuxVarManager(6)
    formula = pblib.VectorClauseDatabase(config)
    geq = 1
    config.set_PB_Encoder(pblib.PB_SORTINGNETWORKS)

    i_const = pblib.IncPBConstraint(wls, pblib.GEQ, 0)
    pb2 = pblib.Pb2cnf(config)

    pb2.encode_inc_initial(i_const, formula, aux_var)
    formula.print_formula("test1.cnf", aux_var.get_biggest_returned_auxvar())

    i_const.encode_new_geq(geq, formula, aux_var)
    formula.print_formula("test2.cnf", aux_var.get_biggest_returned_auxvar())


#
###############################################################################

test_formula()
encode_new_leq(leq_bound: long, VectorClauseDatabase: formula, AuxVarManager: aux_var)

After the initial encoding of an incremental pseudo-boolean constraint, it is possible to encode a new (tighter) bounds with this method. Encodes an incremental constraint with a new leq bound.

Example:

#!/usr/bin/env python3
# -*- coding: utf-8 -*-

from pypblib import pblib

#
###############################################################################

def test_formula():
    wl1 = pblib.WeightedLit(1, 1)
    wl2 = pblib.WeightedLit(2, 1)
    wl3 = pblib.WeightedLit(3, 1)
    wl4 = pblib.WeightedLit(4, 1)
    wl5 = pblib.WeightedLit(5, 1)
    wls = [wl1, wl2, wl3, wl4, wl5]
    config = pblib.PBConfig()
    aux_var = pblib.AuxVarManager(6)
    formula = pblib.VectorClauseDatabase(config)
    leq = 3
    config.set_PB_Encoder(pblib.PB_SORTINGNETWORKS)

    i_const = pblib.IncPBConstraint(wls, pblib.LEQ, 4)
    pb2 = pblib.Pb2cnf(config)

    pb2.encode_inc_initial(i_const, formula, aux_var)
    formula.print_formula("test1.cnf", aux_var.get_biggest_returned_auxvar())

    i_const.encode_new_leq(leq, formula, aux_var)
    formula.print_formula("test2.cnf", aux_var.get_biggest_returned_auxvar())


    #
    ###############################################################################

test_formula()
get_non_inc_constraint -> PBConstraint

Returns a new PBConstraint with the same atributes (weighted literals, comparator and bounds) of the IncPBConstraint which takes as a parameter.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 2)
>>> wl3 = pblib.WeightedLit(3, 2)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 2)
>>> i_constr
+2x1+2x2+2x3<=2
>>> type(i_constr)
<class 'pypblib.pblib.IncPBConstraint'>
>>> constr = i_constr.get_non_inc_constraint()
>>> constr
+2x1+2x2+2x3<=2
>>> type(constr)
<class 'pypblib.pblib.PBConstraint'>
get_geq_inc_constraint() → IncPBConstraint

Takes an incremental pseudo boolean constraint and returns a new IncPBConstraint changing the comparator to a greater-equal. However, the bound does not change. If the greater-equal bound is equal to zero (because the previous incremental restriction had not been assigned any value), the bound will remain zero.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 2)
>>> wl3 = pblib.WeightedLit(3, 2)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 2)
>>> i_constr
+2x1+2x2+2x3<=2
>>> i_constr2 = i_constr.get_geq_inc_constraint()
>>> i_constr2
+2x1+2x2+2x3>=0
get_leq_inc_constraint() → IncPBConstraint

Takes an incremental pseudo boolean constraint and returns a new IncPBConstraint changing the comparator to a less-equal. However, the bound does not change. If the less-equal bound is equal to zero (because the previous incremental restriction had not been assigned any value), the bound will remain zero.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 2)
>>> wl3 = pblib.WeightedLit(3, 2)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.GEQ, 4)
>>> i_constr
+2x1+2x2+2x3>=4
>>> i_constr2 = i_constr.get_leq_inc_constraint()
>>> i_constr2
+2x1+2x2+2x3<=0
get_n() → int

Returns the number of weigted literals in the incremental constraint.

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 3)
>>> wl3 = pblib.WeightedLit(3, -1)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3],
                                      pblib.LEQ, 2)
>>> i_constr.get_n()
3