Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability (Poster Presentation)
Chu Min Li, Wanxia Wei, Yu Li · Theory and Applications of Satisfiability Testing · 2012
Variable properties such as score and age are used to select a variable to flip. The score of a variable x refers to the decrease in the number of unsatisfied clauses if x is flipped. The age ofx refers to the number of steps done since the last time whenx was flipped. If the best variable according to scores in a randomly chosen unsatisfied clause c is not the youngest in c, Novelty [4] flips this variable. Otherwise, with probability p (noise p), Novelty flips the second best variable, and with probability 1-p, Novelty flips the best variable. Novelty+ [1] randomly flips a variable in c with probability wp and does as Novelty with probability 1-wp. Novelty++ [3] flips the least recently flipped variable (oldest) in c with probability dp, and does as Novelty with probability 1-dp. The above approaches just use the current properties of variables to select a variable to flip. These approaches are effective for the problems that do not present uneven distribution of variable and/or clause weights during the search. In other words, problems can be solved using these approaches when there are no clauses or variables whose weight is several times larger than the average during the search [6]. However, when solving hard random or structured SAT problems using these approaches, variable or clause weight distribution is often uneven. In this case, the falsification history of clauses and/or the flipping history of variables during the search should be exploited to select a variable to flip for the problems to be solved. In this paper, we present a noise mechanism that exploits the history information to determine noise p. For a falsified clause c ,l etvar fals[c] denote the variable that most recently falsifies c and let num fals[c] denote the number of the most recent consecutive falsifications of c due to the flipping of this variable. If the best variable in c is not var fals[c], this variable is flipped. Otherwise, the second best variable is flipped with probability p ,w herep is determined as a function of k=num fals[c]: {20,50,65,72,78,86,90,95,98,100} ,i .e.,p=0.2 if k=1, p=0.5 if k=2, ..., p=1 if k ≥ 10. This probability vector was empirically turned using a subset of instances. Another adaptive noise mechanism was introduced in [2] to automatically adjust noise during the search. We refer to this mechanism as Hoos’s noise mechanism. SLS solvers TNM and adaptG 2 WSAT2011 , described in Fig. 1, are both based on Novelty, but use noise p determined by our noise mechanism at each uneven step, and use noise p1 adjusted by Hoos noise mechanism at each even step, to flip the second best variable in the randomly selected unsatisfied clause c when the best variable in c is the youngest in c .I nTNM , a step is even if the variable weight distribution currently is even (e.g., all variable weights are smaller than 10 × the average variable weight). In adaptG 2 WSAT2011 , a step is even if c currently has small weight (e.g., smaller than