Using Decision Procedures Efficiently for Optimization

Abstract

Optimization problems are often solved by making repeated calls to a decision procedure that answers questions of the form "Does there exist a solution with cost at most k?". In general the time required by the decision procedure varies widely as a function of k, so it is natural to seek a query strategy that minimizes the time required to find an (approximately) optimal solution. We present a simple query strategy with attractive theoretical guarantees. In case the same decision procedure is used for multiple optimization problems, we discuss how to tailor the query strategy to the sequence of problems encountered. We demonstrate the power of our query strategy by using it to create (i) a modified version of Sat Plan that finds provably approximately optimal plans quickly and (ii) a modified branch and bound algorithm for job shop scheduling that yields improved upper and lower bounds.