Abstract
Encoding combinatorial problems in terms of propositional logic and using a SAT-solver to obtain a solution has become a common method for tackling hard problems. Although today’s SAT solvers handle very large formulas with hundreds of thousands of clauses, these encodings often become prohibitively large if the underlying instance is large. This makes it necessary to use heuristics for these larger instances, often foregoing the opportunities provided by modern SAT-solvers. I will discuss SAT-based local improvement (SLIM), an approach that combines SAT encodings with a heuristic approach and has been successfully used to obtain very good solutions for huge instances. SLIM starts with a heuristic solution and incrementally improves this solution by applying a SAT-solver to a smaller local problem. I will give an introduction to the general concept and talk about several successful applications including decision tree induction and graph coloring.