# Dynamic Initial Weight Assignment for MaxSAT
## 3 Dynamic Local Search and MaxSAT  
Local search algorithms have proven remarkably successful when applied to solving the propositional Satisfiability (SAT) representation of real-world problems. In general, the local search algorithm begins by assigning random initial values to all the propositional variables (assigning literals the values zero or one) that make up the SAT problem's clauses. It repeatedly works to change the variables' values if that change leads to partial solutions that are closer to the complete solution to the problem. Changing the variables' values is among the most critical factors distinguishing a local search algorithm from others. It consists of two essential parts in most search algorithms: the first part concerns the mechanism of selecting the variable whose value can be changed based on specific conditions (for example, it is possible to refrain from changing the value of a variable if that variable has recently altered its value as in tabu search [8; 9]; for a detailed discussion, see [29]), and the second part focuses on the effectiveness and feasibility of changing the value of the variable and whether the change will lead to approaching optimal solutions to the problem being solved, or at least to new partial solutions closer to the optimal solutions than the current partial solutions. The emergence of the GSAT algorithm in 1992 is among other important reasons that led to the intense interest in Stochastic Local Search (SLS) algorithms. Therefore, since then, many researchers' attention and interests have shifted to studying and examining ways to develop more robust and efficient SLS algorithms. Hence, SLS became one of the main tracks of handling and solving real-world problems. The GSAT algorithm deterministically picks a variable with the best score iteratively and changes (flips) its value while solving an SAT-based problem. Thus, the GSAT algorithm either successfully reaches a solution or runs into a situation where it cannot find any more variables to improve the current partial solution cost (this phenomenon is known as local optima). The deterministic attribute of GSAT was too greedy and led to encountering local optima very frequently. As a result, in the year 1993, two well-known algorithms were introduced to relax the deterministic attribute of GSAT (and to reduce the level of greediness), namely the breakout method and the GSAT+weight algorithm. Both algorithms use weights while searching for a solution to the problem being solved. They also appeared in the same year, but they differ in terms of application. The breakout algorithm was applied to address and solve Constraint Satisfaction Problems (CSP), where the GSAT+weight was mainly applied to handle and solve SAT-based problems. In the SAT community, the GSAT+weight and breakout algorithms are considered (at the time) among the best algorithms, which are robust and scale well while handling SAT problems, and currently, they are considered the core of the well-known Dynamic Local Search (DLS) solvers. DLS solvers follow LS's same underlying general paradigm where the solvers start by a complete, but stochastic instantiation of the variables, then iteratively improving the current cost function (maximizing the number of satisfied clauses) until either a complete solution is reached (i.e., the number of unsatisfied clauses is zero) or the search has reached its time limit. When encountering local minima, DLS solvers use weights assigned to each clause within the formula \(\mathcal{F}\) to calculate the cost of a move \(m\) (flipping a literal value) instead of counting only \(score(m)\).