Adaptive Lookahead for Answer Set Computation

Lookahead is a well-known constraint propagation technique for DPLL-based SAT and answer set solvers. Despite its space pruning power, it can also slow down the search, due to its high overhead. In this paper, this twofold effect is analyzed. On one side, we give characterizations of the problems for which the cause for the reduction of search efficiency shows clearly. On the other we show that problem instances that lie in the phase transition regions often significantly benefit from the use of lookahead. Our analysis leads to a proposal of adaptive lookahead, which performs lookahead according to the learned information during the search. Adaptive lookahead is implemented in one of the best-known answer set solvers, smodels. Our experiments show that adaptive lookahead adapts well to different search environments it is going through.