Hamiltonian Circuit (HC) Domain: Comparison with different encodings

More details about this benchmark can be found in the web page: BENCHMARK PROBLEMS FOR ANSWER SET PROGRAMMING SYSTEMS.

So far we have compared the three systems: ASSAT, Smodels, and DLV, using the same encoding for each of the benchmark problems. Since DLV is designed for disjunctive logic programs and there is an encoding provided on its web site that uses disjunctive rules, and Smodels supports a compact encoding using cardinality constraints, an interesting question is how these systems will compare when they use different encodings. To find out, we did some experiments using the Hamiltonian Circuit benchmark domain.


Encodings

1. The normal encoding: hc.lp( Own to Niemela 1999).
2. Smodels's encoding using cardinality constraints: hc.smodels, originally from here.
3. DLV's disjunctive encoding: hc.dlv, originally from here.


Table -hc.4: Comparison with different encodings, on HC on random graph

problem:
(Has HCs) 		Smodels
(new) 		Smodels DLV DLV
(new) 		ASSAT
(mchaff)
nv50a238 1.03 1.31 1.28 2.55 4.97
nv50a256 --- --- 1.14 2.3 23
nv50a277 1.09 1.57 235.51 --- 1.22
nv50a296 1.12 76.38 --- 101.46 1.37
nv50a326 --- --- --- 3.1 7.31
nv50a360 1.13 1.89 --- --- 30.52
nv50a373 1.25 2.15 2.17 51.15 26.98
nv50a393 --- 2.29 1.7 3.94 11.21
nv50a413 --- --- 3.81 4.22 25.13
nv50a430 1.27 2.39 2.89 4.69 8.82
nv50a456 --- --- 3084.76 --- 85.84
nv50a469 1.32 2.55 2.1 --- 19.64
nv50a485 --- 2.93 2.24 88.78 70.05
nv50a507 10 2.94 2.19 50.92 70.79
nv50a524 1.43 3.23 3.77 11.48 7.53
nv50a552 8.61 3.6 8.37 12.08 4
nv50a565 1.82 3.73 2.97 7.56 12.93
nv60a316 --- --- --- 3.41 14.42
nv60a356 --- --- 6.93 --- 52.47
nv60a414 1.32 2.32 --- 3520.12 13.05
nv60a435 1.43 24.17 3504.83 --- 44.13
nv60a452 1.37 2.67 2.42 --- 82.43
nv60a471 1.4 2.6 2.1 --- 34.87
nv60a485 1.45 3.06 3.46 5.94 6.99
nv60a513 --- --- 10.1 --- 7.53
nv60a526 1.48 3.29 2.28 --- 1327.43
nv60a554 1.59 1769.05 --- --- 33.79
nv60a569 1.6 3.5 --- --- 1.68
nv70a294 1.07 1.4 553.67 2291.74 11.81
nv70a314 1.2 1.56 --- --- 26.11
nv70a335 1.39 1.73 3.72 4.48 240.07
nv70a355 1.32 1.91 --- 4.53 22.84
nv70a372 1.36 2.05 --- --- 3.93
nv70a396 1.43 2.44 --- 4.39 142.67
nv70a413 1.38 2.5 --- 5.51 9.91
nv70a338 1.46 278.72 --- --- 127.54
nv70a452 --- --- 2.1 --- 824.52
nv70a475 2535.6 2.76 --- --- 11.87
nv70a494 1.64 15.47 --- 220.46 73.59
nv70a511 --- --- 32.88 --- 266.45
nv70a535 13.7 3.35 118.79 5492.35 3.24
nv70a549 1.69 3.38 4.13 8.62 299.97
nv70a571 2.09 --- --- --- 332.19
.
SUM 81807.05 74234 122802.3 148705 4426
average 1902.49 1726.39 2855.868 3458.27 102.95
STDEV 3166.163 3060.72 3453.467 3513.84 238.75
unsolved 11 10 16 19 0

In the above figure, nvxay means a graph that had x vertexes and y arcs.

Smodels(New) refers to the performance of Smodels using the new encoding, similarly for DLV(New). The entries for Smodels, DLV and ASSAT(mChaff) are the same as in Table -hc.1.

Yuting Zhao
Last modified: Saturday January 3 2003