By Neng-Fa Zhou (CUNY Brooklyn College & Graduate Center)
Abstract
SAT solvers’ performance has drastically improved during the past 20 years, thanks to the inventions of techniques from conflict-driven clause learning, backjumping, variable and value selection heuristics, to random restarts. SAT has become the backbone of many software systems, including specification languages for model generation and checking, planning, program analysis and test pattern generation, answer set programming, and solvers for general constraint satisfaction problems (CSPs).
In order to fully exploit the power of SAT solvers, a compiler is needed to Booleanize constraints as formulas in the conjunctive normal form (CNF) or some other acceptable form. […] We have developed an optimizing compiler in Picat, called PicatSAT, which adopts the sign-and-magnitude log-encoding for domain variables. For a domain with the maximum absolute value n, it uses log2(n) Boolean variables to encode the domain. If the domain contains both negative and positive values, then another Boolean variable is employed to encode the sign. Each combination of values of the Boolean variables represents a valuation for the domain variable. The addition constraint is encoded as logic adders, and the multiplication constraint is encoded as logic adders using the shift-and-add algorithm. […]Complete paper in PDF