PBLib -- a library for encoding pseudo-Boolean constraints into CNF. PBLib is an easy-to-use and efficient library, written in C++ for translating pseudo-Boolean (PB) constraints into CNF. We have implemented fifteen different encodings of PB constraints. Our aim is to use efficient encodings, in terms of formula size and whether unit propagation maintains generalized arc consistency. Moreover, PBLib normalizes PB constraints and automatically uses a suitable encoder for the translation. We also support incremental strengthening for optimization problems, where the tighter bound is realized with few additional clauses, as well as conditions for PB constraints.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)
- Philipp, Tobias; Steinke, Peter: PBLib -- a library for encoding pseudo-Boolean constraints into CNF (2015)