## 3 Clause Weight in SLS
### Assessment of the Initial Weight Distribution and Its Impact  
To accurately assess the efficacy and the impact of the assignment of the initial weight on the overall performance of a given SLS clause weighting algorithm, we conducted experiments on a wide range of the SAT-based CNF problems obtained from both the SATLIB (dimacs cnf) [45] and the SAT competition benchmarks [46] random track benchmarks. We selected the problems set based on two conditions: first, all the problems are hard to solve, where the ratio of variables-to-clauses is 4.2 (aka, the phase transition region). Second, the problems are of three different sizes, small (e.g., BMS-499), medium (e.g., 4 blocks), and large (e.g., bw_large.d). To conduct our experiment, we used PAWS as the solvingmechanism to gather the weights' statistics at the beginning and during the search. PAWS uses a simple yet efficient additive weighting mechanism for adjusting the weights. It starts by assigning a unit one of weight for each clause in the problem, then iteratively increases the weights of the unsatisfied clauses by one and then, periodically, smooths the weights to prevent unlimited weights growth. We designed the experimental investigation as follow: firstly, we recorded, for each problem, the total number of clauses \(nCl\), and the neighborhood information, (as previously discussed in Section 2, a neighboring area of clause \(cl\) consist of all the clauses that share at least one literal \(\in\) clause \(cl\)), such that, we recorded the minimum neighborhood size \(MinN\), the maximum neighborhood size \(MaxN\), the average neighborhood size \(AvgN\). Also, we calculated the total number of smallest clauses \(cl\) (the size of a clause \(sCl\) is the number of literals within the clause \(cl\)) that have the smallest neighborhood size \(sCL\)\(sesN\), and the smallest clauses with the largest neighborhood size \(sCL\)\(sesN\), and the largest clauses with the smallest neighborhood size \(lCl\)\(sesN\) and finally, the largest clauses with the largest neighborhood size \(lCl\)\(lN\). Our initial observation from the data that are showed in Table 1 reveals that the highest percentage of the clauses are of small size, more specifically 93%, and 99% of which have small neighborhood size, except for the logistics problem where the percentage of small clauses is 91%. Based on the above observations, the SAT-based CNF clauses are categorized into the following four categories:  
1. a small clause in a small neighborhood
2. a small clause in a large neighborhood
3. a large clause in a small neighborhood
4. a large clause in a large neighborhood  
The above four categories are general to any SAT-based CNF problems. However, the fact that some problems clauses are of fixed size, like the 3-CNF problem, therefore, we have came to a conjecture that the first two categories are imperative factors while engineering a general-purpose SLS clause weighting solver. Thus, we ran a further investigation of our problem sets, focusing on the number of clauses weights gain while searching for solutions, focusing on the first two clauses categories' statistics. Out of no surprise, the results, as shown in Figure 1, support our conjecture such that the small clauses, regardless of the size of their neighborhood, were more prone to the fluctuation between satisfied and unsatisfied status.