Encoding Linear Constraints into SAT

Abstract

Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encoding linear constraints to SAT performs poorly in problems with these constraints in comparison to constraint programming (CP) or mixed integer programming (MIP) solvers. But some problems contain a mix of combinatoric constraints and linear constraints, where encoding to SAT is highly effective. In this paper we define new approaches to encoding linear constraints into SAT, by extending encoding methods for pseudo-Boolean constraints. Experimental results show that these methods are not only better than the state-of-the-a..