Lookahead Saturation with Restriction for SAT

We present a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit hard structure.

• Type: Conference
• Year: 2005
• Where: CP
• Authors: Anbulagan, John K. Slaney
• Keywords: CP 2005, Dynamic Equality Weighting, Lookahead Saturation, Neighbourhood Variable Ordering, Programming Languages