Hamiltonian Circuit (HC) Domain

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

We tested three classes of problems: randomly generated graphs, hand-coded hard graphs, and complete graphs. All these are directed graphs that do not have any arcs that go from a vertex to itself, as is usually assumed in work on HC. Since walksat is incomplete, we invented ASSAT(WC) (Walksat+Chaff2): given a SAT instance, try ASSAT(walksat on it first, if it does not return an assignment, then try Chaff2 on it. Another problem with walksat is that it is a randomized system, so its performance may vary from run to run. We address this problem by running it 10 times, and takes the average. Thus in all the tables below, the data on ASSAT(WC) are the averages over 10 runs.


Encoding of Hamiltonain Circuit Problem: hc.lp( Own to Niemela 1999).


HC on random graph

problem:
(Has HCs)		 arc smodels DLV ASSAT
(chaff)		 No. of loading
SAT		 No. of
Loop Formula		 ASSAT
(WC)		 No. of loading
SAT		 No. of
Loop Formula
nv50a240 238 0.58 1.91 29.45 27 27 11.68 34 33
nv50a260 256 200.001 1.58 18.4 12 12 4.85 19 21
nv50a280 277 0.77 --- 8.82 7 7 3.87 13 13
nv50a300 296 72.34 106.34 9.78 6 5 4.03 13 12
nv50a340 326 --- 2.29 151.25 52 53 0.62 1 0
nv50a360 360 1.12 --- 167.68 35 36 1.26 3 2
nv50a380 373 1.33 53 14.05 14 14 7.94 24 25
nv50a400 393 1.45 3.25 47.37 16 16 2.24 6 5
nv50a420 413 --- 3.36 21.85 18 17 3.91 10 9
nv50a440 430 1.55 4.38 11.99 11 10 2.32 6 5
nv50a460 456 --- --- 52.23 36 35 2.11 5 4
nv50a480 469 1.75 --- 10.69 17 17 1.39 3 2
nv50a500 485 2.05 89.03 5.66 7 6 7.5 19 18
nv50a520 507 2.25 53.06 32.36 34 33 4.28 10 9
nv50a540 524 2.43 11.14 3.21 7 6 5.81 14 13
nv50a560 552 2.79 12.15 40.52 28 27 7.34 17 16
nv50a580 565 2.92 6.69 30.65 33 33 2.32 4 3
nv60a320 316 --- 2.67 6.25 11 12 12.32 36 38
nv60a360 356 --- --- 27.07 18 19 12.97 29 35
nv60a420 414 1.5 3511.17 3.73 2 1 2.76 7 6
nv60a440 435 22.34 --- 406.58 61 62 3.94 10 10
nv60a460 452 1.79 --- 67.83 11 10 30.52 58 58
nv60a480 471 1.73 --- 138.08 34 34 4.58 12 11
nv60a500 485 2.19 5.43 98.36 15 15 1.02 1 0
nv60a520 513 --- --- 677.98 52 53 8.85 19 18
nv60a540 526 2.4 --- 10.89 6 6 10.05 22 22
nv60a560 554 1985.02 --- 138.04 34 34 23.08 43 45
nv60a580 569 2.7 --- 1.4 2 1 12.32 46 46
nv70a300 294 0.45 2244 30.26 25 26 0.62 1 0
nv70a320 314 0.61 --- 10.09 7 7 33.45 42 42
nv70a340 335 0.83 4.09 70.91 34 36 9.56 23 23
nv70a360 355 0.93 3.99 6.38 5 5 46.4 46 46
nv70a380 372 1.02 --- 3.02 1 0 3.26 6 5
nv70a400 396 1.38 3.87 97.91 15 17 26.97 48 47
nv70a420 413 1.44 4.85 91.26 38 39 11.24 18 19
nv70a440 338 260.9 --- 60.43 21 21 24.93 42 43
nv70a460 452 --- --- 633.08 26 27 27.1 44 47
nv70a480 475 1.82 --- 226.97 17 16 1.24 2 1
nv70a500 494 14.25 224.44 260.94 42 43 10.47 22 21
nv70a520 511 --- --- 548.73 48 53 13.1 24 24
nv70a540 535 2.24 5516.2 188.39 26 25 68.29 88 90
nv70a560 549 2.26 7.86 51.57 7 6 3.11 6 5
nv70a580 571 --- --- 2757.6 31 32 68.39 85 88
.
SUM 88801.14 163076.8 21669.71 949 954 14944.01 981 980
average 1973.36 3623.93 481.55 21.09 21.2 332.09 21.80 21.78
STDEV 3201.06 3521.14 1526.11 15.62 16.25 1497.99 21.14 22.00
No. of solved 34 24 43 43

In the above figure, nvxay means a graph that had x vertexes and y arcs once it was first randomly generated out. The values in the 2nd column are the numbers of arcs after deleting those arcs which go back to their start-vertexes.


Hand Coded Graph

graph Vertex arc HC? smodels dlv ASSAT
(chaff)		 No. of loading
SAT		 No. of
Loop Formula		 ASSAT
(WC)		 No. of loading
SAT		 No. of
Loop Formula
2xp30 60 316 n 0.34 0.49 0.59 2 2 2.58 2 2.5
2xp30.1 60 318 y 1.14 --- 52.70 51 125 821.88 169.4 403.9
2xp30.2 60 318 y --- --- 51.38 66 120 1185.29 186 330.8
2xp30.3 60 318 y --- --- 51.55 66 120 1669.78 230.7 403
2xp30.4 60 318 n --- --- 5160.72 28 42 4047.50 44.4 70.8
4xp20 80 392 n 0.41 0.68 0.61 2 4 162.87 24.7 44
4xp20.1 80 395 n --- --- 9.60 2 4 9.37 2 4.2
4xp20.2 80 396 y 1.57 --- 7.71 31 74 558.11 133 350.3
4xp20.3 80 396 n 0.42 0.95 15.13 15 19 20.37 13.2 18.2

2xp30 -- 2 copies of p30; 2xp30.i -- 2xp30 + two new arcs;
4xp20 -- 4 copies of p20; 4xp20.i -- 4xp20 + 3-4 new arcs;


Complete graph

complete graph vertex smodels dlv ASSAT
(chaff)		 No. of loading
SAT		 No. of
Loop Formula		 ASSAT
(WC)		 No. of loading
SAT		 No. of
Loop Formula
np10c 10 0.24 0.27 0.24 1 1 0.47 3.5 2.5
np20c 20 3.54 6.02 21.56 46 45 4.81 10.9 9.9
np30c 30 24.18 48.63 8.88 5 4 15.14 9.5 8.5
np40c 40 106.76 228.30 230.9 59 58 49.00 12.1 11.1
np50c 50 417.08 error 857.31 97 96 435.16 41.5 40.5
np60c 60 1046.38 error 72.29 4 3 1139.50 60.5 59.5
np70c 70 2508.26 error 633.67 28 27 640.22 28.0 27.0
np80c 80 4978.3 error 5833.86 122 121 6157 106.5 105.5
np90c 90 --- error --- 3478 60 59

In the above figure, npxc means a complete graph with x vertexes


Hard Jods

In our experiments on randomly generated graphs, we also found 2 graphs, n60e348 and n60e358 which, do not contain the Hamiltonain Circuit, but none of the systems that we tested (Smodels, DLV, ASSAT(X)) could solve them in a time-limit of 2 hours. They are not Hamiltonian for the obvious reason that some of the vertexes in them do not have an arc going out. They both have 60 vertexes, and one has 348 arcs and the other 358.

We found they also gave out 2 hard instances for SAT solvers . None of the SAT solvers that we tested could solve the completions (in CNF) of the logic programs corresponding to these two graphs in the time-limit.


Yuting Zhao
Last modified: Thursday April 11 2002