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.
|Collections||ANU Research Publications|
|Source:||Proceedings of International Conference on Principles and Practice of Constraint Programming (CP 2005)|