1. Introduction
Many realworld problems are of NPcomplete (nondeterministic polynomial) class. In contrast, systematic approaches (based on explicit rules) require exponential time rather than a polynomialtime to reach a solution. A problem is NPcomplete if there is an NP ($np$) problem, and all NP problems are reduced to ($np$) in polynomial time. Therefore, NPcomplete problems are of great interest in computer science because finding an algorithm that could solve any NPcomplete problem implies that there is a generalpurpose algorithm that could solve all NPcomplete problems of the same class.
Metaheuristics methods are widely employed to handle NPcomplete problems with attributes such as uncertainty and vast search spaces. The metaheuristic approach’s main idea is to find a solution with an acceptable quality rather than finding an optimal one. Another characteristic of metaheuristics methods is that they are incomplete such that they do not guarantee to find a solution if one exists. In literature, the metaheuristics methods are classified into globalbased approaches (also known as populationbased approaches) and localbased approaches. Nature designs generally inspire the globalbased metaheuristics to solve optimization problems [
1,
2,
3], such as the Ant Colony Optimization [
4], which was mainly inspired by ants’ actions and behaviors searching for food. Moreover, the Genetic algorithms (GA metaheuristics) [
5] are other examples that were primarily derived from the natural selection process that is based on past knowledge that is stored in many chromosomes (mainly derived from Charles Darwin theory [
6]) and used to make future decisions on the selection process. In recent years, Swarm Intelligence (SI) globalbased metaheuristics have shown significant improvements in the overall process of handling optimization problems, mainly when applied for solving realworld industrial optimization problems such as scheduling [
7,
8], vehicle routing [
9]. The underlying general framework in swarm intelligence depends on a decisionmaking process involving a broad range of information gathered from multiple dimensions and subdomains of the search space. For instance, when searching for a solution using a SI technique, two factors are considered to evaluate the current search stage progress: (1) the improvement of the current search stage cost and (2) the impact of the current search stage on the overall improvement of the objective cost function of the search process.
The other metaheuristic category proposed almost four decades ago and received a high level of researcher’s attention is local searchbased metaheuristics (LS). LS techniques share most of the characteristics of the globalbased metaheuristics such as incompleteness, and the ability to handle NPcomplete optimization problems when covering all possible solution within the search space is not feasible due to a limitation in computational resources. Our focus on this research is local search metaheuristics, specifically the generalpurpose weighting dynamic local search techniques for SAT.
In 1971, the Boolean satisfiability problem (SAT) (also known as propositional satisfiability problem, or SAT for short) was proven to be an NPcomplete as in Reference [
10], which motivated researchers around the world to come up with general mechanisms for solving SAT. However, no such mechanisms exist and engineering a general mechanism to tackle the SAT problem still an open area for research and experimentation. Stochastic local search (SLS) techniques efficiently handle problems encoded into SAT. Therefore, researchers over the decades are motivated to enhance the performance of SLS techniques.
SAT problems are of great interest to researchers as a wide range of realworld problems are encoded into SAT in areas like artificial intelligence such as planning, scheduling, and other areas such as cryptography or bioinformatics, computer theory, engineering, operation research, physics, to mention a few. However, the nature of SLS techniques is that they are incomplete (no guarantee to explore the search space [
11] fully); therefore, they can not prove satisfiability. Nevertheless, almost four decades’ effort pays off as there are many algorithms capable of handling the SAT problem with hundreds of thousands of variables, which was satisfying when formulating and handling the realworld problem into SAT. However, when converted into the SAT problem, the modern realworld problems require solving the SAT problem that is much larger, in much less time than the size of the SAT problems and the solving speed a decade ago. These requirements of the modern realworld problems imposed even more challenges into handling the SAT problem. Therefore, researchers in both tracks: the exact search area (also known as complete or systematic search), and the stochastic local search (also known as optimization search, or incomplete search [
12]), are trying to investigate more efficient algorithms to handle the size (where the hardware is limited) and the speed in which the solution to the SAT problem is satisfying w.r.t both the quality of the solution and the speed of reaching it.
SLS techniques, no matter how sophisticated they are, are either descending directly from or based indirectly on the work of Lin and Kernighan on Local Search (LS), that is, hillclimbing [
13]. The hillclimbing procedure iteratively improves the objective function, where all the violated constraints (clauses in SAT encoded problems in CNF (Conjunctive normal form)) are measured by searching for moves that reduce the total number of violated constraints. For example, while searching for a solution, any local modification (moves) that make a major reduction of the objective function is taken.
The work of Lin and Kernighan showed that hillclimbing successfully reaches solutions when handling problems such as travelling salesman problem and the nqueen problem [
13] However, the hillclimbing algorithm is faced with encountering what is known as local optima, in which there are no moves in the current solution stage that improve the objective function cost, that is, getting stuck in local minima. In Reference [
14], another algorithm that could improve the hillclimbing algorithm was proposed that employs a random walk known as WalkSAT ([
15]).
The random walk addition reduces the level of the hillclimbing algorithm greediness by increasing the level of the randomness through explicitly picking at complete random order any unsatisfied clause (violated constraint) within the current solution stage and flip one of its literals (assign a different value from the variable domain in constraints satisfaction problem (CSP) [
16]). Another algorithm based on the hillclimbing local search algorithm is the greedy local search (GSAT) [
17] algorithm, which generally follows the hillclimbing procedure such that the moves must improve the current objective function cost, with the addition that equalcost moves are permitted with a probability parameter
p (also known as noise as in simulated annealing [
18,
19,
20,
21]).
The GSAT algorithm could prevent the search process from getting stuck in plateaus, which is another drawback of the hillclimbing algorithm. Thus, the GSAT algorithm could continue searching even though the objective function cost is not improving. In other words, GSAT improved the performance of the hillclimbing algorithm and could successfully cope with the hillclimbing level of greediness through the sideway utilization. However, adding the noise to allow the sideway moves does not prevent GSAT from getting stuck in local minima; therefore, GSAT+Restart (GSAT reset), GSAT+Random Walk, and GSAT+Weights were proposed in the year 1993 [
21]. The three variants’ experimental results show that major improvements are gained such that larger problems could be handled, and the speed of reaching feasible solutions was improved. In 1993 also, Paul Morris [
22] proposed a similar clause weighting technique known as Breakout algorithm The GSAT+Weight and the Breakout algorithm became a building block for many clause weightingbased algorithms in SLS due to their efficacy in handling enormous problems and their simplicity w.r.t implementation. Therefore, a large number of weighting SLS algorithms were proposed in the last three decades.
The breakout algorithm and the GSAT+Weight both assign weights (penalties) to all the clauses (constraints) in the formula
$\mathcal{F}$. Initially, the weights are set to 1, then searching for cost improving moves begins such that the objective function (which measures the total number of unsatisfied clauses or violated constraints) is improving, that is, the number of violations is reducing. When the search could not find any cost improving moves, the weights of all violated constraints (unsatisfied clauses) are increased additively as in Reference [
23] or multiplicatively as in Reference [
24]. This paradigm of using weights while searching for a solution is a milestone in local search and artificial intelligence in general due to its implications of handling realworld problems.
In recent years, handling realworld problems through stochastic local search (SLS) techniques has evolved dramatically, which has lead to the production of more sophisticated generalpurpose stochastic local search algorithms. The evolution of SLS varies from proposing simple yet efficient approaches such as tabu search [
25,
26], and simulated annealing [
18,
19,
20]), to more sophisticated approaches such as scatter search [
27], evolutionary algorithms [
28], dynamic local search [
23,
24,
29,
30], and hybrid SLS [
31,
32].
In this paper, we are interested in dynamic local search weighting algorithms, as this family of algorithms forms one of the four generalpurpose mechanisms for solving SAT [
33]. More specifically, we are interested in investigating the setting of the initial weights, as, to the best of our knowledge, the first and only try in this direction was made in Reference [
34] where a new algorithm is proposed by Ishtaiwi et al., known as DDFW(Divide and distribute fixed weights), in which the initial weights were set to 8, instead of 1. Therefore, a crucial question appears here: is there a way to allocate the initial value of the weights so that it optimizes the search process’s performance and reduces the time it takes to reach a solution with higher efficiency than the currently existing algorithms.
In the next
Section 2, we discuss the preliminaries that are used within the paper. In
Section 3, we discuss a general overview of the similarities and differences among the stateoftheart clause weighting SLS solvers. In
Section 3.1, we broadly investigate the initial weight setting impact on the stateoftheart clause weighting SLS. Then, in
Section 4, we propose a new novel mechanism to assign the clauses’ weights dynamically. We show that changing the current method of weight initialization is dramatically improved by our novel method. Then, in
Section 5, we illustrate the improvements experimentally gains by our approach, and then we analyze the results, and then, the conclusion is drawn in
Section 6.
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 SATbased problems. Therefore, our focus is on the stateoftheart 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 statoftheart 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 stateoftheart dynamic SLS solvers that utilize weights, for example, mulLWD+WR [
36], DCCAlm [
37], CSCCSat [
38], BalancedZ [
39],
$Scor{e}_{2}SAT$ [
40], CCAnrSim [
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 stateoftheart SLS algorithms evaluate a the cost of move
m as follows:
where the (
$Makes\left(m\right)$) is the number of currently unsatisfied clauses that will become satisfied by the move
m, and (
$Breaks\left(m\right)$) 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\left(\right)=0$ are taken with probability p (currently known as the noise probability) in most modern generalpurpose stateoftheart 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. A standard fundamental technology shared among the dynamic local search weighting solvers is the use of weights (penalties) such that the search can take nonimproving moves. Taking nonimproving moves play a significant role in the diversification of the search process. Moreover, it helps in either escaping from or preventing the search from encountering local minima (where the objective function ≠ 0, while there is no cost improving moves could be taken).
The clause weighting SLS algorithms initially assign a unit one of weight (also known as penalties) for each clause in
$\mathcal{F}$ (e.g., References [
23,
24,
29,
30,
43]). Then, weights are maintained during the search such that when there is no cost improving moves in the current search stage, weights are modified additively as in Reference [
23] or multiplicatively as in Reference [
24]. Thus, the score(m) is calculated as follows:
where the (
$WeightMakes\left(m\right)$) is the sum of weights of the currently unsatisfied clauses that will become satisfied, and (
$WeightBreaks\left(m\right)$) is the sum of weights of the clauses that are currently satisfied and would become false by the move
m.
3.1. Assessment of the Initial Weight Distribution and Its Impact
To accurately assess the efficacy and the impact of the assignment of the initial weight on the overall performance of a given SLS clause weighting algorithm, we conducted experiments on a wide range of the SATbased CNF problems obtained from both the SATLIB (dimacs cnf) [
45] and the SAT competition benchmarks [
46] random track benchmarks. We selected the problems set based on two conditions: first, all the problems are hard to solve, where the ratio of variablestoclauses is 4.2 (aka, the phase transition region). Second, the problems are of three different sizes, small (e.g., BMS499), medium (e.g., 4blocks), and large (e.g., bw_large.d). To conduct our experiment, we used PAWS as the solving mechanism to gather the weights’ statistics at the beginning and during the search. PAWS uses a simple yet efficient additive weighting mechanism for adjusting the weights. It starts by assigning a unit one of weight for each clause in the problem, then iteratively increases the weights of the unsatisfied clauses by one and then, periodically, smooths the weights to prevent unlimited weights growth. We designed the experimental investigation as follow: firstly, we recorded, for each problem, the total number of clauses
$nCl$, and the neighborhood information, (as previously discussed in
Section 2, a neighboring area of clause
$cl$ consist of all the clauses that share at least one literal ∈ clause
$cl$), such that, we recorded the minimum neighborhood size
$MinN$, the maximum neighborhood size
$MaxN$, the average neighborhood size
$AvgN$. Also, we calculated the total number of smallest clauses
$cl$ (the size of a clause
$sCl$ is the number of literals within the clause
$cl$) that have the smallest neighborhood size
$sCL\&sN$, and the smallest clauses with the largest neighborhood size
$sCL\&lN$, and the largest clauses with the smallest neighborhood size
$lCl\&sN$ and finally, the largest clauses with the largest neighborhood size
$lCl\&lN$. Our initial observation from the data that are showed in
Table 1 reveals that the highest percentage of the clauses are of small size, more specifically 93%, and 99% of which have small neighborhood size, except for the logistics problem where the percentage of small clauses is 91%.
Based on the above observations, the SATbased CNF clauses are categorized into the following four categories:
a small clause in a small neighborhood
a small clause in a large neighborhood
a large clause in a small neighborhood
a large clause in a large neighborhood
The above four categories are general to any SATbased CNF problems. However, the fact that some problems clauses are of fixed size, like the 3CNF problem, therefore, we have came to a conjecture that the first two categories are imperative factors while engineering a generalpurpose SLS clause weighting solver. Thus, we ran a further investigation of our problem sets, focusing on the number of clauses weights gain while searching for solutions, focusing on the first two clauses categories’ statistics. Out of no surprise, the results, as shown in
Figure 1, support our conjecture such that the small clauses, regardless of the size of their neighborhood, were more prone to the fluctuation between satisfied and unsatisfied status.
On the other hand, clauses of considerable neighborhood size were harder to become unsatisfied for two reasons: first, the possibility of a clause to contain a true literal is high. Second, the score of the move (
m), where
m is to flip a literal within a large unsatisfied clause, is high. Furthermore,
Figure 2 illustrates the weights of the small clauses compared to their neighborhood size. It is clearly shown that clauses with smaller neighborhood gained more weight until the solver reached the solution. Also,
Figure 2 show that small clauses, even if they have a large neighborhood, generally gained more weights compared to large clauses, which gained a relatively smaller amount of weight until the solver flipped one of their literals.
The above clause weight assessment indicates that one of the reasons for the fluctuation status of the small clauses (from satisfied to unsatisfied and vice versa) is because of the initial weight assignment where the clause weighting SLS solvers initially treats the clauses equally (assigning a weight of 1 to all clauses), regardless of their size or the size of their neighborhood. Thus, the gap between the weights of the clauses in the weights’ initial assignment is considerable.
To overcome this challenge, the clause weighting SLS solvers adjusts the weights of the clauses multiplicatively (e.g., ESG [
47], SDF [
48], SAPS) or, in most solvers, additively (e.g., PAWS, Sparrow, BalancedZ, YalSAT...etc.). In the next section, we discuss our novel mechanism in assigning the initial clauses weights dynamically, contributing to filling the clauses’ initial gap, which appears due to the initial equal assignment of clauses weights.
4. The Dynamic Initial Weights Assignment in SLS
In the previous section, we discussed the negative effect of the equal assignment of the clauses’ initial weights on SLS solvers’ overall performance. Our experiments show that the small size clauses take a long time to build up weights to become attractive for the search to satisfy them, especially if their neighborhood’s size is large. Secondly, the clauses’ size plays a vital role when calculating the cost function, such that the large clauses are more likely to break more clauses than small clauses if they become unsatisfied. Thus, small clauses remain in their condition (whether satisfied or not satisfied) for longer than necessary time. These factors contribute to prolonging the search period in general. Therefore, we started thinking about developing a mechanism that would fill the gap between weights, which is often considerable, so that the time spent until a small clause build weights is much less.
Our newly innovative algorithm is divided into two main parts. The first is to analyze a set of information from the problem structure that relies on collecting data before starting the search. The other part is to dynamically allocate initial weights for the clauses, based on the outcome from part one.
Table 2 illustrates the problemspecific structural information, as discussed previously. Our novel mechanism starts with the informationgathering based on observations one and two in
Section 3.1. More specifically, we count the total number of clauses (#MinClsS) of the minimumsized clause (MinClS) and the total number of clauses with maximumsized (MaxClsS) of the maximumsized clause (MaxClS). Moreover, we calculate the average clauses size (AvgS) and the total number of averagesized clauses (#AvgS). Using these measures, we designed our mechanism to assign the initial weights as in Algorithm 1. The lines from 2 to 16 of Algorithm 1 show the initial weights allocation based on the clause
$\left(Cl\right)$ size. If the size of
$\left(Cl\right)$ is less than or equal to the arithmetic average of the sizes of the clauses
$\left(AvgClS\right)$ in the problem (which means that the
$\left(Cl\right)$ is of small size), if it is, we check whether
$\left(Cl\right)$ belongs to a small neighborhood
$\left(size\right(Neighbor\left(Cl\right)<=AvgN)$, if so, we assign to the clause
$\left(Cl\right)$ an initial weight equal to the neighborhood size
$size\left(Neighbor\right(Cl\left)\right)$ of the clause
$Cl$. If the size of the clause’s neighborhood is large
$\left(size\right(Neighbor\left(Cl\right)>AvgN)$, we allocate
$\left(Cl\right)$ initial weight with the equivalent of the arithmetic average clauses’ sizes
$\left(AvgClS\right)$. For the clauses of large size
$\left(size\right(Cl)>Avg(ClS)$, we check whether the neighborhood size associated with
$\left(Cl\right)$ is small
$\left(Neighbor\right(Cl)<=AvgN)$; in this case, we allocate the
$\left(Cl\right)$ weight to equal the arithmetic average of the clauses’ sizes
$\left(AvgClS\right)$. Lastly, if the clause is large
$\left(size\right(Cl)>AvgClS)$ and located in a large neighborhood
$\left(Neighbor\right(Cl)>AvgN)$, we assign the initial weight value of
$\left(Cl\right)$ equal to the clause’s size
$size\left(Cl\right)$.
Algorithm 1 DDFW($\mathcal{F}$) + DynamicInitWeight. 
 1:
randomly instantiate each literal in $\mathcal{F}$;  2:
if$size\left(Cl\right)<=AvgClS$then  3:
if $size\left(Neighbor\right(Cl\left)\right)<=AvgN$ then  4:
set the $initWeight\left(Cl\right)$ to $size\left(Neighbor\right(Cl\left)\right)$;  5:
else  6:
set the $initWeight\left(Cl\right)$ to $AvgClS$;  7:
end if  8:
else  9:
if $size\left(Cl\right)>AvgClS$ then  10:
if $size\left(Neighbor\right(Cl\left)\right)<=AvgN$ then  11:
set the $initWeight\left(Cl\right)$ to $AvgClsS$;  12:
else  13:
set the $initWeight\left(Cl\right)$ to $size\left(Cl\right)$;  14:
end if  15:
end if  16:
end if  17:
for each clause ${c}_{a}\in \mathcal{F}$ do  18:
let the weight ${w}_{a}$ of each clause ${c}_{a}$=$InitWeight$(${c}_{a}$);  19:
end for  20:
set the minimum m to the number of false clauses ${c}_{f}\in F$;  21:
set counter i to zero and boolean b to false;  22:
while solution is not found and not timeout do  23:
calculate the list $\mathcal{L}$ of literals causing the greatest reduction in weighted cost $\Delta w$ when flipped;  24:
if ($\Delta w<0$) or ($\Delta w=0$ and probability $\le 15\%$) then  25:
randomly flip a literal in $\mathcal{L}$;  26:
else  27:
for each false clause ${c}_{f}\in \mathcal{F}$ do  28:
select a satisfied same sign neighboring clause ${c}_{n}$ with maximum weight ${w}_{n}$;  29:
if ${w}_{n}<2$ then  30:
randomly select a clause ${c}_{n}$ with weight ${w}_{n}\ge 2$;  31:
end if  32:
if ${w}_{n}>2$ then  33:
transfer a weight of two from ${c}_{n}$ to ${c}_{f}$;  34:
else  35:
transfer a weight of one from ${c}_{n}$ to ${c}_{f}$;  36:
end if  37:
end for  38:
end if  39:
end while

5. Experimental Results and Analyses
To investigate the new mechanism, we designed the experiments to cover a broad range of data sets within the domain of SAT CNFencoded problems. Thus, we categorized the problem sets according to the following factors: First, all the problem sets have been proven to be solvable, which were obtained from the DIMACS problems [
45]. Secondly, according to their hardness level, we classified the problems sets into two subcategories, easy to solve problems and hard to solve problems (according to the phase transition [
49]).
Then we obtained the problem sets accordingly, based on their size. The resulting problem data sets include four subcategories as follows:
small problems that are hard to solve, i.e., flat200hard
small problems that are easy to solve, i.e., BMS499
large problems that are hard to solve, i.e., bw_large.d
large problems that are easy to solve, i.e., g125.18
Table 3 shows the results for the most studied SATencoded problems (e.g., the blocks world problem set (bw) [
24], logistics planning instances, flat graph coloring (flat), uniform random 3SAT instance (uf) and allintervalseries problem (ais)). These problems are relatively small in size, so we have also included large problem sets such as bw_large.d and the graph coloring (g125.17), where both problems are very hard to solve. Furthermore, we have included uniformed 5SAT, and uniform 7SAT problem sets to widen our experimental investigation. For testing the novel dynamic initial weight assignment mechanism, we directly built the mechanism into DDFW (as shown in Algorithm 1) to gain the benefits of adaptive parameters; hence, we spent a shorter time on the implementation and directly ran the experiments without needing to tune the DDFW process. DDFW was one of the first algorithms to classify clauses into two groups, satisfied clauses, and unsatisfied clauses. DDFW algorithm relies on transferring weights between the two groups of clauses by searching for a neighboring satisfied clause and transferring weight from it to an unsatisfied clause. For these properties, we built our mechanism in the DDFW algorithm to take advantage of the process of dividing the clauses into two groups, as it is compatible with our innovative mechanism in terms of relying on searching in neighboring clauses to reach the satisfied clauses.
We began by testing the performance of the dynamic initial weight assignment mechanism. To do so, we compared the original DDFW + dynamic initial weight assignment with other stateoftheart solvers, namely, paws, probSAT, yalSAT, and Score2SAT.
Figure 3 shows the algorithms’ CPU runtime when applied for solving the problem sets. It was clear that DDFW + the dynamic initial weight assignment performed significantly better than DDFW as the ratio indicates (where the ratio in
Table 3 is the performance of ddfw+dynInitWeight gains over ddfw, for example if the ratio is 5 then ddfw+dynInitWeight performed five times better than ddfw). We conducted all the experiments using Ubuntu 18.04 operating systems, an 8th generation I5 with four cores, each of which speed is 2.5 GHz, and 16 GB of memory.
The results show that DDFW+Dynamic initial weight assignment is significantly enhanced when compared to DDFW and PAWS as it performed better in all the problem sets. Especially on the problems bw_large.d, f800hard, f1600hard, flat200hard, the g125.17, and the uf400hard, where the performance was an order of magnitude better. Also, DDFW+Dynamic initial weight assignment performed four times better than DDFW on the unified k5v200 and k7v98 and twice better on the k7v102 problem. Moreover, DDFW+Dynamic initial weight assignment, when compared to other solvers, performed better in 50% of the overall problem sets and performed similarly with the other solvers on the other problem sets. Our dynamic mechanism’s significant performance enhancement could be noticed on large problems such as the g125.17 and problems known to be hardest to solve, such as the f1600hard, f800hard, the uf400hard, the bw_large.d and the uniform problems k5 and k7. Which support our preliminary assessment such that small clauses with either, small or large neighborhood are hard to be satisfied, and take a longer time to build weights. So when they are dynamically assigned the initial weight as per our mechanism, the performance is enhanced.