מיכאל קודיש

This paper introduces a hybrid search method for optimization problems which combines techniques from Local Search methods and from SAT-based methods. At each iteration, the method performs a 'big-step' move on a subset of variables of the current solution. This step is achieved by encoding the big-step itself as an optimization problem and solving it using a SAT (MaxSAT) solver such that the solution of the big-step results in a higher-quality solution to the entire problem. Experimentation illustrates a clear benefit of the approach over both methods: Local Search methods and SAT-based methods.