Adaptive Memory Search Guidance for Satisfiability Problems

Abstract

Satisfiability problems (SAT) are capable of representing many important real-world 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 of ten 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.