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

problems ais*, par8-*-c and uf125-538. R-Novelty was the best-performing algorithm
on the problems flat100-239 and g*, however the results of τ-EO-ISAT2 on these
problem instances were also quite competitive. Intuitively, this could be explained by
the high connectivity inherent to the structure of these instances that involves much
more difficulties in recycling an old model when new clauses are added. On the prob-
lems ii8*, the best average success rate was achieved by τ-EO-ISAT2, but with a
significantly higher cost than R-Novelty.

Table 1. Results of τ-EO-ISAT on ISAT1instances

Problem id n m Success

rate/ 20

CPU time # Flips

Mean Std Mean Std

20
18
7
2
20
20
20
20
20
20
20
5
20
20
20
20
20
20
20
20
20
20
8
3.60

0.4400
6.8452
6.6520
9.3290
0.0023
0.0179
0.0820
1.2400
0.0142
4.6325
7.8312
16.1210
0.9200
9.5780
1.3650
8.4500
2.4520
6.5642
0.1762
0.3320
1.7328
0.4210
1.7620
8.2540

0.0320
1.6505
2.1420
0.0562
0.0005
0.0012
0.0015
0.0054
0.0006
0.3235
0.5350
2.6453
0.0030
1.4210
0.0450
1.4620
0.3700
1.1260
0.0560
0.0065
0.1045
0.1540
0.2030
0.1054

8800.4
39292.5
8115.0
42638.0
95.0
155.8
328.7
1126.2
328.6
5340.2
45653.4
4800.3
624.3
5800.6
712.5
1912.5
1415.2
1846.5
3623.5
8264.0
25605.2
9725.4
37640.4
54762.0

1245.2
6564.0
1824.9
2562.8
0.0
0.7
65.4
32.1
15.1
525.6
3540.6
2945.7
2.4
234.8
26.5
185.1
164.0
138.8
325.8
237.5
1968.4
2154.7
7682.0
1542.5

ais6
ais8
ais10
ais12
ii8a1
ii8a2
ii8a3
ii8a4
ii8b1
ii8b2
ii8b3
ii8b4
ii8c1
ii8c2
ii8d1
ii8d2
ii8e1
ii8e2
par8-1-c
par8-2-c
par8-3-c
par8-4-c
par8-5-c
flat100-239
(100 inst.)
uf125-538
(100 inst.)
g125-17
g125-18
g250-15
g250-20

61
113
181
265
66
180
264
396
336
576
816
1068
510
950
530
930
520
870
64
68
75
67
75
300

581
1520
3151
5666
186
800
1552
2798
2068
4088
6108
8214
3065
6689
3207
6547
3136
6121
254
270
298
266
298
1117

538 19.25 0.6875 0.3260 9665.3 792.0

125

2125
2250
3750
7250

66272
70163
233965
454622

14
20
18
16

142.9450
1.4585
0.6326
186.5020

12.7620
0.9500
0.9455
20.5490

2051374.0
24056.9
11615.2
1959751.8

158549.1
18669.4
15857.6
232450.8

τ-EO-ISAT1 performed worse than the other two algorithms on all the instances
taking significantly longer time. The intuitive explanation for that low performance is
that an ISAT1 instance is a series of problems with incremental ratios of clauses to
variables, where the first ones are relatively easy to satisfy (few clauses and many