## 3 Clause Weight in SLS  
As we discussed previously, the two main building blocks for almost all weighting local search algorithms are the GSAT+Weight and the Breakout algorithm. However, the GSAT+Weight algorithm was designed to handle the boolean satisfiability (SAT) problems, which is the subject of this research as we only consider the SAT-based problems. Therefore, our focus is on the state-of-the-art clause weighting algorithms driven directly as an improvement of the GSAT+Weight algorithm, or the algorithms that conceptually employ the underlying technique of the GSAT+Weight mechanism. The stat-of-the-art solvers that use different variants of the weighting strategy of the GSAT+Weight mechanism are known as Dynamic Local Search weighting solvers. There are many examples of the state-of-the-art dynamic SLS solvers that utilize weights, for example, mulLWD+WR [36], DCCAlm [37], CSCCSat [38], BalancedZ [39], \(Score_{2}SAT\)[40], CCArSim [41], CryptoMiniSAT [42], Sparrow [43], MapleCOMSPS_LRB_VISDIS [42], and previously DLM [30], SAPS [24], PAWS [23] and DDFW [34]. The underlying technology designed in GSAT is that in each step of the search, a move (\(m\)) is taking if \(m\) reduces the total number of unsatisfied clauses. As we previously discussed in Section 2, a clause \(cl\) consists of the disjunct of some literals or their negation (propositional variable); if \(cl\) is (unsatisfied), then none of its literals is true. A move is to change the value of a literal within \(cl\) (known as the flip) from true to false or vice versa. A decision of which literal within \(cl\) must be taken based on an evaluation function. Some algorithms consider how many clauses will become unsatisfied by flipping a literal as in (e.g., probSAT algorithm [44]). However, in general, most of the state-of-the-art SLS algorithms evaluate a the cost of move \(m\) as follows:  
\[score(m)=Makes(m)-Breaks(m), \tag{1}\]  
where the (\(Makes(m)\)) is the number of currently unsatisfied clauses that will become satisfied by the move \(m\), and (\(Breaks(m)\)) is the number of the clauses that are currently satisfied and would become false by the move \(m\). The Score is the change of the objective function during the current stage of the search process if the move \(m\) is performed. A score(m) is either a positive number, which means the move (\(m\)) will satisfy a maximum number of clauses if taken. A negative score of the move (\(m\)) means (\(m\)) will make more unsatisfied clauses than satisfied ones if taken. In some cases, the score(m) is equal to zero, which means the move (\(m\)) will cause the search to move entirely in a plateau (also known as sideway moves). The best case scenario is that the score(m) is always a positive value, but it is not always the case, and the search will face a situation where the score(m) is either zero or a negative number. Handling the three possible scenarios of the value of the score(m) is one of the imperative characteristics that differentiate solvers from each other, for example. The breakout algorithm would not permit moves with score zero or negative scored moves (highest level of greediness). Another example is the WalkSAT, where moves are taken, regardless of their score, with probability \(p\), when the score(m) is equal to zero or a negative value, for all possible moves in the current position during the search. However, sideways moves, where \(score()=0\) are taken with probability \(p\) (currently known as the noise probability) in most modern general-purpose state-of-the-art SLS solvers. SLS techniques follow the same basic general process when applied for solving a CNF formula \(\mathcal{F}\). They start by randomly assigning random binary values to all the literals in \(\mathcal{F}\). Then, iteratively, search for ways to improve the current objective function by finding cost improving moves through the employment of different techniques and heuristics. One of which is the clause weighting technique.