# Dynamic Initial Weight Assignment for MaxSAT
## 3 Dynamic Local Search and MaxSAT
### DDFW and the Dynamic Initial Weight Assignment  
[PERSON] et al. in the year 2005 [28] introduced the Divide and Distribute Fixed Weight (DDFW) into the area of dynamic local search weighting solvers. Unlike other clause weighting algorithms, where two steps maintain the weights, the increment step and the decrement step, DDFW combines the two steps into one single step. DDFW starts with a random assignment of the variables and iteratively works on violated (unsatisfied clauses) using weights. The novel idea behind DDFW categorizes the clauses into satisfied and unsatisfied clauses. Based on this categorization, the algorithm transfers the weights from the satisfied clauses to unsatisfied ones when a local minimum is encountered (a situation where no cost improving moves are found). Thus, satisfied clauses no longer need weights. The weight increment and weight decrement operations are performed in one step. Moreover, weights are transferred from within the clauses' neighborhoods. For instance, a satisfied clause (\(Cl\_sat\)) with weight \(w\) will donate the weight to unsatisfied clause \(Cl\_unsat\) if \(\exists\) a literal \(l\in(Cl\_sat\) and \(Cl\_unsat)\).  
In a more recent study, in [24], a dynamic initial weight assignment mechanism was introduced based on an extensive survey of the SAT problem's general structures such as the size of a clause and its neighborhood (InitWeight). In the study, the clauses were categorized into four categories: clauses that are small and have a large neighborhood, clauses that are large and have a large neighborhood, clauses that are large and have a large neighborhood, and clauses that are large and have a large neighborhood. Then, the initial weights were dynamically assigned to each clause, according to the clause category (as in Algorithm 1, Lines 1-16). For instance, if the clause is small in size and has a large neighborhood, it may need more weight to be attractive for the search cost function and allow it to break (unsatisfying) some clauses in its neighborhood. The study concluded that the dynamic initial weight assignment could significantly improve the performance of a DLS solver. This mechanism was implemented in DDFW, and DDFW was adjusted to have the best cost reached within the search and time (Algorithm 1, Lines 25-28).  
```
1:randomly instantiate each literal in \(\mathcal{F}\);
2:if\(size(Cl)<=\textit{ArgCSIS}\)then
3:if\(size(Neighbor(Cl))<=\textit{ArgN}\)then
4: set\(initWeight(Cl)\) to \(size(Neighbor(Cl))\);
5:else
6: set\(initWeight(Cl)\) to \(\textit{ArgCSIS}\);
7:endif
8:else
9:if\(size(Cl)>\textit{ArgCSIS}\)then
10:if\(size(Neighbor(Cl))<=\textit{ArgN}\)then
11: set\(initWeight(Cl)\) to \(\textit{ArgCSIS}\);
12:else
13: set\(initWeight(Cl)\) to \(size(Cl)\);
14:endif
15:endif
16:endif
17:for each clause \(c_{s}\in\mathcal{F}\)do
18: let the weight \(w_{a}\) of each clause \(c_{a}=InitWeight(c_{a})\);
19:endfor
20: set the best cost \(C_{\textit{out}}\) to \(\infty\);
21:while\(C_{\textit{out}}>C_{\textit{in}}\) and no timeout do
22: find and return a list \(\mathcal{L}\) of literals causing the greatest reduction in weighted cost \(\Delta w\) when flipped;
23:if\((\Delta w<0)\) or \((\Delta w=0\) and probability \(\leq 15\%)\)then
24: randomly flip a literal in \(\mathcal{L}\);
25:if (number of false clauses in \(\mathcal{F}_{\textit{in}}<C_{\textit{out}}\)) then
26:\(C_{\textit{out}}=\) number of false clauses;
27:\(\mathcal{F}_{\textit{out}}=\mathcal{F}_{\textit{in}}\);
28:endif
29:else
30:for each false clause \(c_{f}\)do
31: select a satisfied same sign neighboring clause \(c_{k}\) with maximum weight \(w_{k}\);
32:if\(w_{k}<2\)then
33: randomly select a clause \(c_{k}\) with weight \(w_{k}\geq\textit{InitWeight(c_{k})}\);
34:endif
35: transfer a weight of 1 from \(c_{k}\) to \(c_{f}\);
36:endfor
37:endif
38:endwhile
```  
**Algorithm 1** DDFW+InitMaxSAT(\(\mathcal{F}_{\textit{in}}\), \(\mathcal{F}_{\textit{out}}\), \(C_{\textit{in}}\), \(C_{\textit{out}}\)).