Anbulagan, AnbuSlaney, John KPeter van Beek2015-12-102015-12-10October 1-9783540292388http://hdl.handle.net/1885/39185We 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.Keywords: Benchmarking; Dynamic programming; Function evaluation; Heuristic methods; Problem solving; Benchmark problems; Dynamic equality weighting (DEW); Lookahead saturation (LAS); Neighbourhood variable ordering (NVO); Computer programming200510.1007/11564751_532024-04-21