Satisfiability and integer programming as complementary tools

Satisfiability (SAT) and integer linear programming (ILP) are two related NP-complete problems. They both have a lot of important applications. We study the effectivenessof using them as a complementary tool to each other. We propose three different ILP formulations to solve SAT and compare them with state-ofthe- art SAT solvers Berkmin and zchaff. On the other hand, we give two methods to solve ILP by using SAT solvers. In both cases, we achieve speed-ups of several orders for most of our tested examples.