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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Karpiński, Michał; Piotrów, Marek: Encoding cardinality constraints using multiway merge selection networks (2019)
- Yip, Ka Wa; Xu, Hong; Koenig, Sven; Kumar, T. K. Satish: Quadratic reformulation of nonlinear pseudo-Boolean functions via the constraint composite graph (2019)
- Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: PySAT: A Python toolkit for prototyping with SAT oracles (2018)
- 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)
- Kautz, Henry; Selman, Bart: The state of SAT (2007)