An Evolutionary Local Search Method for Incremental Satisfiability - Artificial Intelligence and Symbolic Computation - page 147

At this optimal value, the best fitness variables are not completely excluded from
the selection process and hence, more space configurations can be reached so that
greatest performance can be obtained.

3 -EO for SAT

{ }

Given a SAT problem instance of n Boolean variables X = x , x ,...,

x

and m

1 2

() m

clauses

= . A variable fitness λ i is defined as the negation of the total
number of clauses violated by

CF

C

i

x :

()

∑

(3)

λ = − # unsat x = − 1

i i

() x ∈ C and C v = 0

i j j

()

The best fitness is λ = 0 and the worst one is λ = − m . The cost function C S

i i

consists of the individual cost contributions λ i for each variable x i . In order to maxi-
mize the total number of satisfied clauses,

()

C S has to be minimized. Thus,

(4)

()

∑ =

n
i

C S = −

1 λ

i

Algorithm τ-EO-SAT
1.

Randomly generate a solution S . Set Sbest = S .

2. If S satisfies Clauses then return ( S ).

3. Evaluate λ i for each x i in Variables according to Equation 3.

4. Rank x i according to λ i from the worst to the best.

5. Select a rank j according to Equation 1.

6. Set S' = S in which the truth value of x j is flipped

() ( )

7. If C S ′ < C Sbest then Set Sbest = S' .

8. Set S = S' .
9. If the number of steps does not exceed MaxSteps return to Step 2.
10. Return (No model can be found).
End τ-EO-SAT

Fig. 1. Genericτ-EO algorithm for SAT

Figure 1 provides the basic outlines of the algorithm τ-EO for SAT. Let Variables ,
Clauses , MaxSteps and τ be respectively the set of variables, the set of clauses, the
given bound for iteration steps and the free parameter of EO.
(i) Line 1. The search begins at a random truth assignment S and the current best
assignment, Sbest , is set to S .
(ii) Line 2. S is returned as a model if it satisfies Clauses .
(iii) Lines 3-4. The variable individual fitnesses are evaluated and sorted using a
Shell sort.