A Translation of Pseudo-Boolean Constraints to SAT
Olivier Bailleux, Yacine Boufkhad, Olivier Roussel · Journal on Satisfiability Boolean Modeling and Computation · 2006
This paper introduces a new CNF encoding of pseudo-Boolean constraints, which allows unit propagation to maintain generalized arc consistency. In the worst case, the size of the produced formula can be exponentially related to the size of the input c