BoolVar/PB v1.0, a java library for translating pseudo-Boolean constraints into CNF formulae

TL;DR

BoolVar/PB v1.0 is a Java library that efficiently translates pseudo-Boolean constraints into CNF formulas, supporting multiple encoding schemes and extensibility for various applications in SAT solving.

Contribution

This work introduces an open-source Java library that offers flexible, tag-based translation of pseudo-Boolean constraints into CNF, with easy extensibility for new encoders and formats.

Findings

Supports multiple encoding schemes

Allows tagging of input constraints for flexible translation

Easily extendable with new encoders and formats

Abstract

BoolVar/PB 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.