Information Technology Reference
In-Depth Information
5 Experimental Evaluation
In this section, we present an empirical evaluation of τ-EO-ISAT on ISAT instances
obtained from both random and structured SAT instances. In order to compare the
ISAT formulation considered in this work and that introduced by Hooker [14], two
different types of ISAT instances were generated from each SAT instance. The first
one denoted ISAT1, was obtained as follows. Let ISAT1 be an empty set of clauses.
At each time one randomly chosen clause from the SAT instance was added to the
ISAT1 instance and the resulting problem was solved. The series of problems was
solved incrementally until all clauses had been added or no model for the current
problem was found. The second ISAT instance, denoted ISAT2, was generated by
randomly splitting the related SAT instance into two subsets
ϕ
and
ϕ
of
m
and
P
S
m
=
m
−
m
clauses, respectively. Finding a model for
ϕ
is a necessary condition
S
P
P
before solving the ISAT2 instance.
The SAT benchmarks were taken from the DIMACS [25] and SATLIB [24] ar-
chives. Six groups of satisfiable SAT instances were considered : ais* (4 instances of
all interval series problem), ii8* (14 instances of Boolean circuit synthesis problem),
par8-*-c (5 instances of learning the parity function problem), flat100-239 (100 in-
stances of SAT-encoded graph colouring problem), uf125-538 (100 random 3-SAT
instances) and g* (4 large instances of hard graph coloring problem). To have a refer-
ence point, we tested the performance of WalkSAT algorithm with the heuristic R-
Novelty [18], which is one of the best-performing variant of the WalkSAT algorithm
for SAT problem. The program code of WalkSAT was taken from the SATLIB ar-
chive [24]. The algorithm τ-EO-ISAT was coded in C and all experiments were per-
formed on a 2.9 GHz Pentium 4 with 2 GB RAM running Linux. We ran
τ
-EO-ISAT
on ISAT1 and ISAT2 instances with the parameter
set to 1.4 according to approxi-
mately optimal parameter setting [20]. ISAT2 instances were generated setting
m
P
to
0.5
m
. R-Novelty (WalkSAT with -rnovelty parameter) was run with a noise parame-
ter
p
set to 0.6 as suggested in [18]. The programs were run 20 times on each instance
with a maximum of 100000 flips allowed to solve each one except for the large prob-
lem instances g*, where a time limit of 300 seconds was allowed at each run.
The results achieved by τ-EO-ISAT on ISAT1 and ISAT2 instances are presented
in Tables 1 and 2, respectively. Table 3 presents the results obtained with R-Novelty
on related SAT instances.
n
and
m
denote the number of variables and clauses, re-
spectively. For each instance, we give the success rate over 20 runs, the mean CPU
time and the mean number of flips to find a solution and their respective standard
deviations. Table 4 summarizes our results in terms of average success rate, average
CPU time and average number of flips to solve each problem class. τ-EO-ISAT1 and
τ-EO-ISAT2 refer to the algorithm τ-EO-ISAT on ISAT1 and ISAT2 instances, in
that order. Mean CPU times related toτ-EO-ISAT2 include mean CPU times needed
to find a model for
τ
.
In terms of average success rate, average CPU time and average number of flips at
finding a solution τ-EO-ISAT2 outperformed τ-EO-ISAT1 and R-Novelty on the
ϕ
P
Search WWH ::
Custom Search