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 effectiveness of using them as a complementary tool to each other. We propose three different ILP formulations to solve SAT and compare them with state-of-the-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.