# Dynamic Initial Weight Assignment for MaxSAT
## 3 Dynamic Local Search and MaxSAT
For instance, assuming flipping literal \(l\) would lead to breaking more clauses (a broken clause is the one with all of its literals being false) than making clauses (a satisfied clause), the clauses' weights may make this move attractive to the search heuristic, as illustrated in the following formula:  
\[Score(m)=WeightMakes(m)-WeightBreaks(m) \tag{4}\]  
To elaborate more, assume that a literal \(l\) occurs in three unsatisfied clauses and the only true literal in five satisfied clauses. If we are to flip literal \(l\), the \(score(m_{l})\) would be equal to \(-2\) (it will break five clauses and make three). Therefore, the move would not be made as it would increase the cost function. However, if the three false clauses have been unsatisfied for a relatively long time and the weights were employed, the three clauses' weights would be increased during the period in which they were unsatisfied. Therefore, the score function of the move \(m\) (flipping \(l\)) might be a positive integer that would force the move \(m\) to be made by the heuristic. Based on the above discussion of weight utilization, a crucial issue arose regarding maintaining weights during the search. As such, a question arises about how long a clause can hold weights after it becomes satisfied. Another question to be addressed is when a clause weight must be increased. Among others (as allowing equal cost moves or what is known as noise [23; 30; 31; 32]), these issues have been addressed and investigated exhaustively. As a result, significant improvements and many DLS solvers were proposed (see mulLWD+WR [33], DCCAlm [34], CSCCSat  
Ref. [35], BalancedZ [36], \(Score_{2}SAT\)[37], CCAnrSim [38], CryptoMiniSAT [39], Sparrow [27], MapleCOMSPS_LRB_VISDIS [39], and previously DLM [13], SAPS [14], PAWS [15], and DDFW [28; 40]). Typically, DLS weighting algorithms start with the initial assignment of weights for all the clauses fixed to unit one before searching for solutions, and then, the weights are adjusted during the search. In general, deciding when to increase the weights or reduce them is the current search stage status. For instance, if the search progresses in finding closer to optimal solutions, the weights are reduced; otherwise, the search encountering local minima and weights is incremented in all the unsatisfied clauses. This general approach constitutes an underlying mechanism for all weighting DLS (mentioned above). DLS solvers are applied to handle unweighted MaxSAT in a straightforward approach. The only modification to be considered instead of searching for a complete solution (where all the clauses are satisfied), DLS solvers are modified to keep track of the best partial solution reached (in other words, keeping track of the number of maximum satisfied clauses reached so far) and at which time. For instance, an unweighted MaxSAT problem's clauses are equally treated (regardless of whether they must be satisfied as partial MaxSAT), so an SAT solver could be applied to solve unweighted MaxSAT [41]. However, the unweighted MaxSAT problem is impractical when handling real-world problems encoded in CNF, since real-world problems often have different types of constraints. Therefore, a more practical real-world MaxSAT representation was proposed in [42] where the clauses were categorized into two categories: (1) clauses that must be satisfied, known as hard clauses (hard constraints), and (2) clauses that are preferably satisfied, known as soft clauses (soft constraints). MaxSAT with hard and soft clauses is known as Partial MaxSAT (PMS) and has a wide range of applications in various research fields and real-world situations. A variant of PMS known as Weighted Partial MaxSAT (WPMS) [43] uses weights for the hard and soft clauses. The distinction between the hard and soft clauses is established by assigning a large number of weights for all hard clauses in the WPMS problem where the soft clauses are initially assigned unit one of weight at the starting stage of the search.