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

lished experimentally its effectiveness by testing two types of ISAT instances derived
from SAT benchmark problems. Indeed, one or more clauses can be added to the
original problem either incrementally one at a time (ISAT1) or together at the same
time (ISAT2). The experimental results suggest that the algorithm is more efficient on
ISAT2 instances and at least as competitive as WalkSAT with R-Novelty heuristic
for SAT. However, this work should be understood as an initial investigation and
further experiments are necessary to both study the behaviour of the algorithm on
large benchmark instances, and compare its performance with those of other methods.
Additionally, we plan to investigate the effect of varying the ratio of the clauses being
added as well as the free parameter of τ-EO on the performance of the algorithm.
Finally, this work can be used as an algorithmic framework for incremental solving
with other SAT solvers.

Table 4. Summary of average results for each problem group

Problem class ais* ii8* par8-*-c flat100-239 uf125-538 g*

Average Success rate / 20

11.75
14.00
12.75

18.92
19.92
19.28

17.60
19.00
18

3.60
5.30
7.10

19.25
19.55
19.40

17.00
19.25
20.00

τ-EO-ISAT1
τ -EO-ISAT2

R-Novelty

Average CPU time secs

5.8165
2.3776
3.5189

4.2335
1.5015
0.7923

0.8848
0.2567
0.6945

8.2540
5.2050
4.2600

0.6875
0.4382
0.5500

82.8845
50.3991
51.9900

τ -EO-ISAT1

τ-EO-ISAT2
R-Novelty

Average flips

τ -EO-ISAT1

τ-EO-ISAT2
R-Novelty

24711.47
10246.87
13373.5

5009.98
2169.69
633.04

16971.69
6016.76
10116.45

54762.00
42435.70
37574.00

9665.30
4359.60
4850.20

1011699.40
485685.10
350624.15

Acknowledgment

The author is grateful to the anonymous referees for their valuable comments and
suggestions.

References

1. Adami, C.: Introduction to Artificial Life. Springer-Verlag Berlin Heidelberg New York
(1999)
2. Bak, P., Tang, C., Wiesenfeld, K.: Self-Organized Criticality: An Explanation of 1/ f noise.
Physical Review Letters, V86 N23, (1987) 5211-5214
3. Bak, P., Sneppen, K.: Punctuated Equilibrium and Criticality in a Simple Model of Evolu-
tion. Physical Review Letters, 59. (1993) 381-384
4. Bak, P.: How Nature Works. Springer-Verlag, Berlin Heidelberg New York (1996)