# Dynamic Initial Weight Assignment for MaxSAT
## 1 Introduction  
Maximum Satisfiability (MaxSAT) is a general optimization NP-hard [1] form of the well-known NP-complete propositional Satisfiability (SAT) [2]. Given a propositional SAT encoded problem in Conjunctive Normal Form (CNF), where CNF consists of a set of conjunctive clauses and each clause consists of a set of disjunctive literals (propositional variables) or their negations, a solution to a MaxSAT problem is the one with the maximum number of satisfied clauses. One important role that makes MaxSAT of particular interest within the SAT community is that a solution is accepted with some optimality level. Thus, handling real-world problems by employing MaxSAT methods is more practical, as many, if not most, real-world problems are unsatisfiable (an assignment that satisfies all the clauses does not exist). As a matter of fact, in [3], the Local Search (Local Search (LS)) solving techniques were mainly designed to handle the MaxSAT problems. Then, the techniques were extended to solve the SAT problems as in [4]. Therefore, instead of searching for a completely optimal solution, MaxSAT solving methods aim to find the assignments with the maximum number of satisfied clauses. MaxSAT has many applications in real-world problems such as planning, timetabling, scheduling, bioinformatics, and intelligent routing, which are imperative in artificial intelligence or its related fields. Therefore, MaxSAT is of exceptional interest to researchers in the SAT community, as finding a general-purpose solver that could find near-optimum solutions to MaxSAT is an open research area with significant potentials. In the literature, there are two main tracks for handling MaxSAT problems: (1) the complete track (also known as the systematic or exhaustive track) such as EvalMaxSAT [5] (which was implemented in the MSCGMaxSAT solver [6]), such as RC2, the winner of the unweighted and weighted main track MaxSAT evaluation in 2018 [7], or (2) the incomplete track, such as Stochastic Local Search (Stochastic Local Search (SLS)) like tabu search [8; 9], simulated annealing, scatter search [10], evolutionary algorithms [11], dynamic local search [12; 13; 14; 15], and hybrid SLS [16; 17]. While both tracks, complete and incomplete, share the same goal of finding a solution for the MaxSAT problem, they differ widely on how to achieve this goal. The complete track algorithms exhaustively search the problem space. Therefore, a conclusion is drawn about whether the problem has an optimum solution if one exists. Unlike complete algorithms, the SLS algorithms explore the search space stochastically until they discover a good solution within the time constraints. Therefore, they are faster at finding a solution and incur less computational cost. However, they compromise on finding an optimum solution and cannot conclude that a good solution does not exist. On the one hand, the tradeoff incurred by the search completeness is that it is computationally costly when applied to solving large problems where it struggles with the computational resources and meeting the time constraints. However, the complete search algorithms can guarantee finding an optimal solution if one exists. On the other hand, the incomplete attribute of Track 2 led to the fact that the SLS algorithms can handle large problems and find good (near-optimum solutions) in relatively acceptable computational cost and time constraints with the expense of reaching optimality. SLS solvers belong to a family of techniques known as metaheuristic methods, where the solvers are either global search-based or Local Search-based techniques (LS). In general, global-based search is derived from and mainly inspired by natural design. For example, Ant Colony Optimization (Ant Colony Optimization (ACO)) is a known algorithm to handle SAT optimization problems [18], which is inspired by ants while searching for food (which involves keeping track of the colony and finding the best paths to a food source.