# Boolvar/Pb V1.0, A Java Library For Translating Pseudo-Boolean Constraints Into Cnf Formulae

Olivier Bailleux, Université de Bourgogne November 8, 2018

## Abstract 1

BoolVar/pb **v1.0** is an open source **java** library dedicated to the translation of pseudo-Boolean constraints into cnf formulae. Input constraints can be categorized with tags. Several encoding schemes are implemented in a way that each input constraint can be translated using one or several encoders, according to the related tags. The library can be easily extended by adding new encoders and / or new output formats. It is available at **http://boolvar.sourceforge.net/**.

## 1 Introduction

Let us begin by an introductory exemple, which consists in translating the constraint 5x1 + 3x2 +x3 ≤ 8 **into**
a cnf **formula. At first, an input model must be created as follows:**
InputModel m = new **InputModel** ( ) ;
Then, the three variables x1, x2, x3 can be created as an array of instances of the class **Variable**.

Variable [ ] x = new **Variable** [ 3 ] ;
for ( int i=0; i<3; i++) x [ i ] = new **Variable** ( ) ;
The input constraint is composed of literals that can be produced from the variables. Each literal is an instance of the class **Literal**.

Literal [ ] lits = new **Literal** [ 3 ] ;
lits [ 0 ] = x [ 0 ] . **getPosLit** ( ) ; lits [ 1 ] = x [ 1 ] . **getNegLit** ( ) ; lits [ 2 ] = x [ 2 ] . **getPosLit** ( ) ;
Before to create the input constraint, we have to define the coefficients related to each literal and the tag that will be assigned to this constraint. Note that it is allowed to assign several tags to the same constraint.

For example, setTags(1,3) will assigns the tags 1 and 3 to the upcoming constraints that **will be created**
until the next call of **setTags**.

int [ ] **coeffs** = { 5 , 3 , 1 };
setTags ( 1 ) ;
To complete the building of the input model, it only remains to create the input constraint, which is simplified by using the static factory method makeLeq**, and add it to the model.**
Constraint q = makeLeq ( coeffs , **lits** , 8 ) ;
m . **addConstraint** ( q ) ;
At this time, the input model is created. It can be print to the **screen for verification purpose.**
System . out . println ( m . **toString** ( ) ) ;
Now, the input model must be translated to an output problem, **namely a** cnf **formula. This suppose to** create an instance of the class CNFProlem **in the following way:**
OutputProblem out = new **CNFProblem** ( ) ;
arXiv:1103.3954v1 [cs.AI] 21 Mar 2011