A compact encoding of pseudo-Boolean constraints into SAT

Abstract

Many different encodings for pseudo-Boolean constraints into the Boolean satisfiability problem have been proposed in the past. In this work we present a novel small sized and simple to implement encoding. The encoding maintains generalized arc consistency by unit propagation and results in a formula in conjunctive normal form that is linear in size with respect to the number of input variables. Experimental data confirms the advantages of the encoding over existing ones for most of the relevant pseudo-Boolean instances. © 2012 Springer-Verlag.