# A New Look at BDDs for Pseudo-Boolean Constraints

arXiv: https://arxiv.org/abs/1401.5860 · HTML: https://mlsanity.com/paper/1401.5860/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Jan 2014.

## Built on by (most cited first, 8 of 8)

- [Optimal Decision Diagrams for Classification](https://mlsanity.com/paper/2205.14500/) (2022)
- [FastDOG: Fast Discrete Optimization on GPU](https://mlsanity.com/paper/2111.10270/) (2021)
- [SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints](https://mlsanity.com/paper/2110.08068/) (2021)
- [Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints](https://mlsanity.com/paper/2307.09342/) (2023)
- [PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas](https://mlsanity.com/paper/2312.15877/) (2023)
- [Solving Cyclic Antibandwidth Problem by SAT](https://mlsanity.com/paper/2601.04239/) (2026)
- [A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints](https://mlsanity.com/paper/2101.01953/) (2021)
- [Exact and approximate determination of the Pareto set using minimal correction subsets](https://mlsanity.com/paper/2204.06908/) (2022)

## Abstract (arXiv)

Pseudo-Boolean constraints are omnipresent in practical applications, and thus a significant effort has been devoted to the development of good SAT encoding techniques for them. Some of these encodings first construct a Binary Decision Diagram (BDD) for the constraint, and then encode the BDD into a propositional formula. These BDD-based approaches have some important advantages, such as not being dependent on the size of the coefficients, or being able to share the same BDD for representing many constraints. We first focus on the size of the resulting BDDs, which was considered to be an open problem in our research community. We report on previous work where it was proved that there are Pseudo-Boolean constraints for which no polynomial BDD exists. We also give an alternative and simpler proof assuming that NP is different from Co-NP. More interestingly, here we also show how to overcome the possible exponential blowup of BDDs by phcoefficient decomposition. This allows us to give the first polynomial generalized arc-consistent ROBDD-based encoding for Pseudo-Boolean constraints. Finally, we focus on practical issues: we show how to efficiently construct such ROBDDs, how to encode them into SAT with only 2 clauses per node, and present experimental results that confirm that our approach is competitive with other encodings and state-of-the-art Pseudo-Boolean solvers.