Journal
ARTIFICIAL INTELLIGENCE
Volume 158, Issue 1, Pages 1-26Publisher
ELSEVIER
DOI: 10.1016/j.artint.2004.04.001
Keywords
search; local search; backbone; backbone guided search; configuration landscape; Boolean satisfiability; maximum Boolean satisfiability
Categories
Ask authors/readers for more resources
Boolean satistiability (SAT) and maximum satisfiability (Max-SAT) are difficult combinatorial problems that have many important real-world applications. In this paper, we first investigate the configuration landscapes of local minima reached by the WalkSAT. local search algorithm, one of the most effective algorithms for SAT. A configuration landscape of a set of local minima is their distribution in terms of quality and structural differences relative to an optimal or a reference solution. Our experimental results show that local minima from WalkSAT form large clusters, and their configuration landscapes constitute big valleys, in that high quality local minima typically share large partial structures with optimal solutions. Inspired by this insight into WalkSAT and the previous research on phase transitions and backbones of combinatorial problems, we propose and develop a novel method that exploits the configuration landscapes of such local minima. The new method, termed as backbone-guided search, can be embedded in a local search algorithm, such as WalkSAT, to improve its performance. Our experimental results show that backbone-guided local search is effective on overconstrained random Max-SAT instances. Moreover, on large problem instances from a SAT library (SATLIB), the backbone guided WalkSAT algorithm finds satisfiable solutions more often than WaIkSAT on SAT problem instances, and obtains better solutions than WalkSAT on MaxSAT problem instances, improving solution quality by 20% on average. (C) 2004 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available