Information Technology Reference
In-Depth Information
Table 3. Results of R-Novelty on SAT benchmark instances
Problem id
n
m
Success
rate/ 20
CPU time
# Flips
Mean
Std
Mean
Std
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
20
19
6
6
20
20
20
20
20
20
18
12
20
20
20
20
20
20
20
20
20
20
10
7.10
0.0984
3.3941
4.9402
5.6430
0.0015
0.0097
0.0260
0.4724
0.0522
0.9451
1.8500
2.1050
0.2378
1.2482
0.6200
1.8550
0.6850
0.9850
0.0760
0.1405
0.9550
1.5304
0.7710
4.2600
0.0062
0.8450
0.6376
1.2640
0.0001
0.0001
0.0075
0.0710
0.0150
0.0548
0.9640
0.7571
0.0001
0.8440
0.0118
0.0330
0.0235
0.1482
0.0050
0.0095
0.2050
0.1225
0.0860
0.9520
2185.8
22065.4
8590.0
20652.8
36.0
90.4
270.0
400.5
115.9
815.4
2366.5
2725.0
174.0
229.1
210.2
564.5
355.0
510.2
2540.5
2115.0
16630.0
22440.8
6856.0
37574.0
84.4
5490.2
1262.5
1850.1
0.0
0.0
10.2
85.1
52.5
152.0
1175.3
901.5
0.0
1.0
5.0
78.5
12.0
15.0
536.4
450.2
1285.0
672.0
1448.4
3715.0
125
538
19.40
0.5500
0.1060
4850.20
722.0
2125
2250
3750
7250
66272
70163
233965
454622
20
20
20
20
71.4670
1.6651
0.7520
134.1025
5.6390
0.2405
0.9460
7.6200
931675.2
12608.4
4632.0
453581.0
98821.0
5732.1
28730.2
110836.5
ported include times needed to find a model for
. Hence, the results presented
suggest that ISAT2 is a promising approach for incremental solving.
ϕ
P
6 Conclusion
In this paper, we have presented a stochastic local search algorithm for solving the
incremental satisfiability problem (ISAT). The satisfiability of the dynamic problem
is maintained by recycling the current model of a sub-problem when new clauses are
added. Local search repairs are performed by an Extremal Optimization algorithm
based on the theory of self-organized criticality of many natural systems. We estab-
Search WWH ::




Custom Search