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).


Table -hc.1: HC on random graph

problem:
(Has HCs) 		. Smodels DLV ASSAT
(chaff)		 No. of loading
SAT		 No. of
Loop Formula		 ASSAT
(WC)		 No. of loading
SAT		 No. of
Loop Formula
nv50a238 1.31 2.55 4.97 6 7 7.65 10.1 10.3
nv50a256 --- 2.3 23 15 13 15.02 20.3 20.4
nv50a277 1.57 --- 1.22 0 1 6.76 10.5 11
nv50a296 76.38 101.46 1.37 0 1 9.75 15.8 15.9
nv50a326 --- 3.1 7.31 14 15 14.53 28 26.9
nv50a360 1.89 --- 30.52 19 20 5.74 10.8 11.2
nv50a373 2.15 51.15 26.98 36 35 5.86 11.8 12.3
nv50a393 2.29 3.94 11.21 6 7 4.57 7.6 8.2
nv50a413 --- 4.22 25.13 11 11 18.08 27.9 28.1
nv50a430 2.39 4.69 8.82 10 11 7.88 15.9 16.2
nv50a456 --- --- 85.84 47 47 11.76 19.9 20.6
nv50a469 2.55 --- 19.64 24 25 5.07 10.7 11.2
nv50a485 2.93 88.78 70.05 31 32 7.73 12.8 13.3
nv50a507 2.94 50.92 70.79 37 38 4.62 7.3 8.2
nv50a524 3.23 11.48 7.53 14 15 7.77 13.8 14.7
nv50a552 3.6 12.08 4 7 8 12.28 17 17.5
nv50a565 3.73 7.56 12.93 15 16 4.26 6.2 7.1
nv60a316 --- 3.41 14.42 11 10 18.24 26 24.6
nv60a356 --- --- 52.47 23 23 17.39 18.6 17.8
nv60a414 2.32 3520.12 13.05 3 4 17.84 24.3 23.2
nv60a435 24.17 --- 44.13 9 10 15.59 25.2 23.9
nv60a452 2.67 --- 82.43 11 11 37.77 41.6 40.3
nv60a471 2.6 --- 34.87 9 10 9.33 13.1 13.6
nv60a485 3.06 5.94 6.99 12 12 15.35 24.2 24.8
nv60a513 --- --- 7.53 2 3 18.18 25.2 25.1
nv60a526 3.29 --- 1327.43 24 23 26.15 34.7 34.4
nv60a554 1769.05 --- 33.79 31 30 16.1 23 23.1
nv60a569 3.5 --- 1.68 0 1 13.65 19.3 18.9
nv70a294 1.4 2291.74 11.81 6 7 27.16 12.8 12.3
nv70a314 1.56 --- 26.11 11 11 27.61 18.3 17.4
nv70a325 1.73 4.48 240.07 41 37 17.25 19.5 18.3
nv70a355 1.91 4.53 22.84 9 10 24.55 13.3 14.1
nv70a372 2.05 --- 3.93 4 5 10.74 9.7 10
nv70a396 2.44 4.39 142.67 41 39 33.19 32.3 31
nv70a413 2.5 5.51 9.91 3 4 31.07 18.8 18.9
nv70a428 278.72 --- 127.54 43 42 46.6 38.1 36.3
nv70a452 --- --- 824.52 26 23 46.38 40.9 38.5
nv70a475 2.76 --- 11.87 6 5 23.47 29 28.8
nv70a494 15.47 220.46 73.59 30 30 21.39 27.7 27.2
nv70a511 --- --- 266.45 23 24 14.46 17.5 17.8
nv70a535 3.35 5492.35 3.24 6 6 18.89 25.3 24.8
nv70a549 3.38 8.62 299.97 25 25 14.12 19.4 19.5
nv70a571 --- --- 332.19 9 9 19.35 19.5 19.9
.
SUM 74234 148705 4426 710 716 731 863 857
Average 1726.39 3458.27 102.95 16.51 16.65 17 20.09 19.94
STDEV 3060.72 3513.84 238.75 13.11 12.51 10.48 8.94 8.34
Unsolved 10 19 0 0

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


Table -hc.2: 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 1.28 1.39 1.57 2 2 4.69 2.2 2
2xp30.1 60/318 y 2.07 --- 205.9 254 99 732.05 369.4 149.3
2xp30.2 60/318 y --- --- 70.41 213 128 1041.6 378.1 222.6
2xp30.3 60/318 y --- --- 70.54 213 128 774.45 322.5 187.5
2xp30.4 60/318 n --- --- --- 5983.48 18 12.7
4xp20 80/392 n 1.27 1.51 1.54 5 2 4.52 4.1 2
4xp20.1 80/395 n --- --- 8.3 4 2 18.76 4.1 2
4xp20.2 80/396 y 2.43 --- 39.08 248 95 471.63 333.8 126.7
4xp20.3 80/396 n 1.24 1.79 9.12 9 5 19.84 17.7 13.2

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


Table -hc.3: Complete graph

complete graph smodels dlv ASSAT
(chaff)		 No. of loading
SAT		 No. of
Loop Formula		 ASSAT
(WC)		 No. of loading
SAT		 No. of
Loop Formula
c10 1.14 1.26 1.52 2 3 1.26 3.3 4.3
c20 5.15 8.12 5.92 11 12 3.02 3.3 4.3
c30 29.48 58.69 6.24 2 3 16.43 8.9 9.9
c40 115.43 242.72 11.2 1 2 77.13 18.3 19.3
c50 414.62 850.12 21.07 1 2 399.04 54 55
c60 1091.13 2075.26 275.5 37 38 1488.31 76.8 77.8
c70 2598.65 4831.81 1170.44 94 95 2281.4 87.6 88.6
c80 5173.11 --- 5905.4 249 250 4396.5 116.4 117.4
c90 --- --- 208.84 4 5 2844.21 57.9 58.7
c100 --- --- 2732.49 66 67 3162.76 46.875 47.125

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: Saturday January 3 2003