Switching among Non-Weighting, Clause Weighting, and Variable Weighting in Local Search for SAT

One way to design a local search algorithm that is effective on many types of instances is allowing this algorithm to switch among heuristics. In this paper, we refer to the way in which non-weighting algorithm adaptG2 WSAT+ selects a variable to flip, as heuristic adaptG2 WSAT+, the way in which clause weighting algorithm RSAPS selects a variable to flip, as heuristic RSAPS, and the way in which variable weighting algorithm V W selects a variable to flip, as heuristic V W. We propose a new switching criterion: the evenness or unevenness of the distribution of clause weights. We apply this criterion, along with another switching criterion previously proposed, to heuristic adaptG2 WSAT+, heuristic RSAPS, and heuristic V W. The resulting local search algorithm, which adaptively switches among these three heuristics in every search step according to these two criteria to intensify or diversify the search when necessary, is called NCV W (Non-, Clause, and Variable Weighting). Experimental ...

• Type: Conference
• Year: 2008
• Where: CP
• Authors: Wanxia Wei, Chu Min Li, Harry Zhang
• Keywords: Artificial Intelligence, CP 2008, Heuristic Adaptg2 Wsat+, Heuristics, Local Search Algorithm