Python Pseudo-Boolean library

This library offers a comprehensive set of utilites to work with pseudo-boolean formulas within Python.

This module provides bindings to the PBLib – A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF.

Note

You can build the pypblib via:

python3 setup.py build

You can install the pypblib via:

python3 setup.py install

Overview

Pseudo-Boolean Constraint

PBLib provides classes that allows us to encode pseudo-Boolean constraints.

The first to know is the WeightedLit class.

Class WeightedLit

The WeightedLit class is used to represent the literals of a pseudo-Boolean constraint, including their weight.

If we take the following pseudo-Boolean constraint as an example:

2 x1 + 3 x2 + 1 x3 <= 3

We can represent their literals as follows:

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 2)
>>> wl2 = pblib.WeightedLit(2, 3)
>>> wl3 = pblib.WeightedLit(3, 1)
>>> print(wl1, wl2, wl3)
(1, 2) (2, 3) (3, 1)

An operator (inequality) is also required to represent the constraint.

Comparator

The Comparator represents the inequality symbols. It is a set of constants. You can treat the comparator as it were an enum: { LEQ, GEQ, BOTH }

• LEQ (less-equal)
• GEQ (greater-equal)
• BOTH (less-equal & greater-equal)

Now we have everything we need to instantiate a constraint.

Class PBConstraint

The PBConstraint class is used to represent a pseudo-Boolean constraint. Receives a list of WeightedLit, a comparator and a bound.

Following the previous example we can generate a constraint as follows:

>>> constr = pblib.PBConstraint([wl1, wl2, wl3], pblib.LEQ, 3)
>>> constr
+2x1+3x2+x3<=3

However, depending on the comparator, two limits may be necessary. When using the BOTH comparator, a single limit is equivalent to strict equal. Therefore, in case working with a constraint such as the following,

1<=+2x1+3x2+x3<=3

it is necessary to use the BOTH comparator and two bounds. The Pblib also provides a constructor for the PBConstraint in these cases. This takes a list of WeightedLit, a comparator, the less-equal bound and the greater-equal bound.

>>> constr_2 = pblib.PBConstraint([wl1, wl2, wl3], pblib.BOTH,
                                    3, 1)
>>> constr_2
1<=+2x1+3x2+x3<=3

class PBConfig

An intance of the PBConfig class contains the configuration for all options in the PBLib.

For more information about the default configuration and all configuration options, you can see all details here.

class Pb2cnf

The class Pb2cnf is the main interface to encode a pseudo-boolean constraint.

The Pb2cnf constructor takes a PBConfig as a parameter. However, if PBConfig is omitted the default configuration will be used.

For a simple interface you can use one of the following methods:

encode_at_most_k (literals: [int], k: long, formula: [], first_free_variable: int) -> int

encode_at_least_k (literals: [int], k: long, formula: [], first_free_variable: int) -> int

encode_leq (weights: [long], literals: [int], k: long, formula: [], first_free_variable: int) -> int

encode_geq (weights: [long], literals: [int], k: long, formula: [], first_free_variable: int) -> int

encode_both (weights: [long], literals [int], leq: long, geq: long, formula: [], first_free_variable: int) -> int

But for a more sophisticated interface you should use, besides the PBConstraint, a VectorClauseDatabase and an AuxVarManager.

If your encode has only one constraint, you can use one of the methods listed above. However, if you have several constraints, you will need to use the following method:

encode (constr: PBConstraint, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)

class AuxVarManager

The constructor of AuxVarManager class takes an integer as parameter.

The auxiliary variable manager, returns fresh variable to the encoder. Therefore it must be initialized with the first fresh variable.

class VectorClauseDatabase

The constructor of VectorClauseDatabase class takes an PBConfig as parameter.

The clause database is a container of clauses. Every clause that is added is saved into a vector of clauses.

If we take the followings pseudo-Boolean constraints as example (this is a dummy instance; only for demonstration purposes):

1 x1 + 1 x2 + 2 x3 <= 2

1 x4 + 2 x5 - 1 x6 >= 1

The following is a encoding full example:

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 1)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> wl3 = pblib.WeightedLit(3, 2)
>>> constr_1 = pblib.PBConstraint([wl1, wl2, wl3], pblib.LEQ, 2)
>>> wl4 = pblib.WeightedLit(4, 1)
>>> wl5 = pblib.WeightedLit(5, 2)
>>> wl6 = pblib.WeightedLit(6, -1)
>>> constr_2 = pblib.PBConstraint([wl4, wl5, wl6], pblib.GEQ, 1)
>>> config = pblib.PBConfig()
>>> pb2 = pblib.Pb2cnf()
>>> aux_var = pblib.AuxVarManager(7)
>>> formula = pblib.VectorClauseDatabase(config)
>>> pb2.encode(constr_1, formula, aux_var)
>>> formula
Num. Causes: 12
==============================
7 0
-7 8 0
-2 8 0
-7 -2 9 0
-1 8 0
-7 -1 9 0
-2 -1 9 0
-7 -2 -1 10 0
-3 11 0
-9 11 0
-3 -9 12 0
-12 0
==============================

>>> pb2.encode(constr_2, formula, aux_var)
>>> formula
Num. Causes: 24
==============================
7 0
-7 8 0
-2 8 0
-7 -2 9 0
-1 8 0
-7 -1 9 0
-2 -1 9 0
-7 -2 -1 10 0
-3 11 0
-9 11 0
-3 -9 12 0
-12 0
13 0
-13 14 0
-6 14 0
-13 -6 15 0
4 14 0
-13 4 15 0
-6 4 15 0
-13 -6 4 16 0
5 17 0
-15 17 0
5 -15 18 0
-18 0
==============================

Incremental Pseudo-Boolean Constraint

In this part we will assume that you already know some of the basic PBLib classes that are used to generate the encoding of a pseudo-Boolean constraint. These classes, WeightedLit , Comparator , PBConfig, Pb2cnf , AuxVarManager and VectorClauseDatabase , are also used to encoding incremental pseudo-boolean constraints. Hence, if you are not familiar with these classes, go to Pseudo-Boolean Constraint before continuing to read this part.

Class IncPBConstraint

The IncPBConstraint behaves very much like PBConstraint. The main difference is that it allows, when the coding is already generated, to make it more restrictive. To do this, instead of using the encode(…) method of Pb2cnf class, we will use this other method:

encode_inc_initial (inc_constr: IncPBConstraint, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)

When we already have the encoding, we can increase the restriction using the methods provided by the IncPBConstraint class, depending on the case:

encode_new_geq (geq_bound: long, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)

encode_new_leq (leq_bound: long, formula: VectorClauseDatabase, aux_var_manager: AuxVarManager)

Let’s see an example:

1 x1 + 1 x2 + 1 x3 <= 2

>>> from pypblib import pblib
>>> wl1 = pblib.WeightedLit(1, 1)
>>> wl2 = pblib.WeightedLit(2, 1)
>>> wl3 = pblib.WeightedLit(3, 1)
>>> i_constr = pblib.IncPBConstraint([wl1, wl2, wl3], pblib.LEQ, 2)
>>> config = pblib.PBConfig()
>>> pb2 = pblib.Pb2cnf()
>>> aux_var = pblib.AuxVarManager(4)
>>> formula = pblib.VectorClauseDatabase(config)
>>> pb2.encode_inc_initial(i_constr, formula, aux_var)
>>> formula
Num. Causes: 8
==============================
-3 4 0
-2 4 0
-3 -2 5 0
-1 4 0
-3 -1 5 0
-2 -1 5 0
-3 -2 -1 6 0
-6 0
==============================
>>>
>>> i_constr.encode_new_leq(1, formula, aux_var)
>>> formula
Num. Causes: 9
==============================
-3 4 0
-2 4 0
-3 -2 5 0
-1 4 0
-3 -1 5 0
-2 -1 5 0
-3 -2 -1 6 0
-6 0
-5 0
==============================

Example, from OPB to CNF file

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

import sys
import re

from pypblib import pblib


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

PBLIB_OPS = {'<=': pblib.LEQ, '>=': pblib.GEQ, '=': pblib.BOTH}

HEADER_RE = re.compile(r'(.*)\s*#variable=\s*(\d+)\s*#constraint=\s*(\d+)\s*')
TERM_RE = re.compile(r'([+-]?\d)\s+x(\d+)')
IND_TERM_RE = re.compile(r'([>=|<=|=]+)\s+([+-]?\d+)')


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

def transform_pb_to_cnf(pb_formula_path: str):
    config = pblib.PBConfig()
    aux = pblib.AuxVarManager(1)
    pb2cnf = pblib.Pb2cnf(config)
    formula = pblib.VectorClauseDatabase(config)

    with open(pb_formula_path, 'r') as f:
        m = HEADER_RE.match(f.readline())
        aux.reset_aux_var_to(int(m.group(2)) + 1)

        reader = (l for l in map(str.strip, f) if l and l[0] != '*')
        for line in reader:
            wl = [pblib.WeightedLit(int(l), int(w))
                for w, l in TERM_RE.findall(line)]
            op, ind_term = IND_TERM_RE.search(line).groups()

            constraint = pblib.PBConstraint(wl, PBLIB_OPS[op], int(ind_term))
            pb2cnf.encode(constraint, formula, aux)
    return formula, aux


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

if __name__ == '__main__':
    f, aux = transform_pb_to_cnf(sys.argv[1])
    f.print_formula("test.cnf", aux.get_biggest_returned_auxvar())

Example, from OPB to WCNF file

import sys
import re
from pypblib import pblib

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

DEFAULT_FILE_NAME = "test_wcnf.cnf"
op = {'<=': pblib.LEQ, '>=': pblib.GEQ, '=': pblib.BOTH }
_sum_soft_weights = 1

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

def read_opb(path):

    config = pblib.PBConfig()
    aux = pblib.AuxVarManager(1)
    hard = pblib.VectorClauseDatabase(config)
    soft = []
    pb2 = pblib.Pb2cnf(config)

    f = open(path,'r')
    for line in f:

        if len(line) == 0: continue
        if '#variable=' in line:
            aux.reset_aux_var_to(int(re.findall(r"\d+", line)[0]) + 1)
        if line[0] == '*': continue
        if 'min:' in line:
            soft = re.findall(r"[-\d]+", line)
            continue

        # This is linear equation
        lq = re.findall(r"[-\d|>=|<=|=]+", line)
        wl = [pblib.WeightedLit(int(lq[i+1]), int(lq[i])) for i,e in enumerate(lq[:-2]) if(i%2 == 0)]

        pb2.encode(pblib.PBConstraint(wl, op[lq[-2]], int(lq[-1])), hard, aux)

    f.close()

    return aux, soft, hard
#
###############################################################################

def write_cnf(file_path, aux, soft, hard):

    with open(file_path, 'w') as f:
        f.write("p wcnf " + str(aux.get_biggest_returned_auxvar()) + " " + str(hard.get_num_clauses() + int(len(soft)/2)) \
               + " " + str(sum(int(e) for i,e in enumerate(soft) if(i%2 != 0)) + 1) + '\n')
        for i, e in enumerate(soft):
            if(i%2 == 0):
                global _sum_soft_weights
                _sum_soft_weights += abs(int(soft[i]))
                if(int(soft[i]) < 0):
                    f.write(str(abs(int(soft[i]))) + " " + str(int(soft[i+1])) + " 0\n")
                else:
                    f.write(str(abs(int(soft[i]))) + " " + str(-int(soft[i+1])) + " 0\n")

        v_form = hard.get_clauses()

        for c in v_form:
            tmp = ""
            for i in c:
                tmp += str(i);
            f.write(str(_sum_soft_weights) + " " + tmp + " 0\n")

    f.close()
#
###############################################################################


if __name__ == '__main__':

    file_path = DEFAULT_FILE_NAME
    if len(sys.argv) > 2:
        file_path = argv[2]

    aux, soft, hard = read_opb(sys.argv[1])
    write_cnf(file_path, aux, soft, hard)

Index

• 1. Class WeightedLit
  • 1.1. Constructor
  • 1.2. Method summary
  • 1.3. Method details
• 2. Class PBConstraint
  • 2.1. Constructor
  • 2.2. Methods summary
  • 2.3. Methods details
• 3. Class IncPBConstraint
  • 3.1. Constructor
  • 3.2. Methods summary
  • 3.3. Methods details
• 4. Class PBConfig
  • 4.1. Constructor
  • 4.2. Methods summary
  • 4.3. Methods details
• 5. Class AuxVarManager
  • 5.1. Constructor
  • 5.2. Methods summary
  • 5.3. Methods details
• 6. Class VectorClauseDatabase
  • 6.1. Constructor
  • 6.2. Methods summary
  • 6.3. Methods details
• 7. Class Pb2cnf
  • 7.1. Constructor
  • 7.2. Methods sumary
  • 7.3. Methods details