Adaptive memory search guidance for satisfiability problems

Abstract

Satisfiability problems (SAT) are capable of representing many important realworld problems, like planning, scheduling, and robotic movement. Efficient encodings exist for many of these applications and thus having good solvers for these problems is of critical significance. We look at how adaptive memory and surrogate constraint processes can be used as search guidance for both constructive and local search heuristics for satisfiability problems, and how many well-known heuristics for SAT can be seen as special cases. We also discuss how adaptive memory learning processes can reduce the customary reliance on randomization for diversification so often seen in the literature. More specifically, we look at the tradeoff between the cost of maintaining extra memory search guidance structures and the potential benefit they have on the search. Computational results on a portfolio of satisfiability problems from SATLIB illustrating these tradeoffs are presented.© 2005 by Kluwer Academic Publishers.