# hss: HCP Solver based on Scarab and Sat4j

## Overview

### Requirements

- Java version 1.7.* or higher.
- Scala version 2.11.*

### How to use it

- Download the latest version.
- Edit file "hss" for your environment.
- Exec the following

$ ./hss [options] [inputFile]

### Options

-h : show this help -undirected : treat input graph as undirected graph -conf <solver conf> : use <solver conf> for sat4j -v : verbose mode (generate Hamiltonian Cycle if SAT). -post : use post process (cycle merge) -no-learnt : remove learnt clauses per iteration -jelia2014 : use jelia2014 configuration (-undirected, -no-learnt

### Output Format (Line of "CSV")

1st column: 2nd column: Instance Name 3rd column: #nodes 4th column: #arcs (or #edges if -undirected option is ON) 5hh column: Result 6th column: #Vars 7th column: #Const 8th column: #Iterations 9th column: #Cycles Found 10th column: Validation Result

### Example1 (for directed graph)

$ ./hss -v ex/directed/rnd_00100_01.col OPTIONS,NativePBEncoder,Sat4j,Default,ex/directed/rnd_00100_01.col,false,false,true,false,false Parsing Graph Done. Encoding Done. Iteration 0: 16 found cycles are merged into 16 -- (16 sub cycles are added in total) Iteration 1: 6 found cycles are merged into 6 -- (22 sub cycles are added in total) Iteration 2: 3 found cycles are merged into 3 -- (25 sub cycles are added in total) Iteration 3: 4 found cycles are merged into 4 -- (29 sub cycles are added in total) Iteration 4: 6 found cycles are merged into 6 -- (35 sub cycles are added in total) Iteration 5: 4 found cycles are merged into 4 -- (39 sub cycles are added in total) Iteration 6: 2 found cycles are merged into 2 -- (41 sub cycles are added in total) Iteration 7: 1 found cycles are merged into 1 -- (42 sub cycles are added in total) Validate Hamiltonicity --- OK s SAT 69->53->27->34->98->40->5->33->8->12->38->79->66->68->41->95->39->25->81->43->15->90->84->49->58->73->18->97->21->67->24->74->55->71->26->87->93->14->17->50->7->94->65->22->89->86->47->77->62->72->45->37->59->96->80->28->31->76->85->42->57->4->51->46->2->20->3->23->6->99->61->83->35->16->60->70->91->44->56->36->1->11->82->63->100->92->30->19->9->32->13->48->29->88->10->52->78->75->64->54->69 CSV,ex/directed/rnd_00100_01.col,100,650,SAT,650,538,8,42,OK

### Example2 (for undirected graph)

$ ./hss -v -undirected ex/undirected/myciel6.col OPTIONS,NativePBEncoder,Sat4j,Default,ex/undirected/myciel6.col,true,false,true,false,false Parsing Graph Done. Encoding Done. Iteration 0: 3 found cycles are merged into 3 -- (3 sub cycles are added in total) Iteration 1: 6 found cycles are merged into 6 -- (9 sub cycles are added in total) Iteration 2: 2 found cycles are merged into 2 -- (11 sub cycles are added in total) Iteration 3: 6 found cycles are merged into 6 -- (17 sub cycles are added in total) Iteration 4: 4 found cycles are merged into 4 -- (21 sub cycles are added in total) Iteration 5: 4 found cycles are merged into 4 -- (25 sub cycles are added in total) Iteration 6: 1 found cycles are merged into 1 -- (26 sub cycles are added in total) Validate Hamiltonicity --- OK s SAT 69->33->61->30->59->7->92->9->86->8->28->66->25->64->46->62->29->49->40->51->39->56->35->54->37->94->41->70->42->52->43->58->44->50->36->53->27->68->26->60->24->67->34->65->1->88->95->78->16->73->21->74->17->81->18->71->20->75->19->93->15->80->4->91->3->83->47->90->23->82->2->87->11->89->5->84->10->85->6->72->14->77->12->79->22->76->13->55->45->57->38->48->32->63->31->69 CSV,ex/undirected/myciel6.col,95,755,SAT,1510,1135,7,26,OK

### Download

- hss-v1-0-0.tar.gz
- IHCP.tar.gz (old version)
- Except the Scala compiler version (2.10.2 -> 2.11.1), this version is the same one used in JELIA 2014 paper.

### Publication

- Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem.
- Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara and Naoyuki Tamura.
- In: Eduardo Fermé and Joäo Leite (eds.), Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA 2014),
- Lecture Notes in Artificial Intelligence, Vol.8761, pp.684-693, Springer, 2014.

- you can find supplemental tables here.

### Note

- This software is distributed under the BSD License. See LICENSE file.
- hss-<version>.jar includes Sat4j package.
- We really appreciate the developers of Sat4j!

## Benchmarks

- undirected graphs
- Instances used in
- Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem. Takehide Soh, Daniel Le Berre, Stephanie Roussel, Mutsunori Banbara, and Naoyuki Tamura.
- You can find the pre-print (full-version) of the paper here.

- All graphs are undirected.
- File format (.col)
- 1st line denotes the number of nodes and edges.
- If graph contains an edge \(\{i, j\}\) then "e i j" will appear in a row if \((i < j)\), otherwise "e j i".
- For instance, 3 nodes graph whose edges are \(\{1, 2\},\{2, 3\}\) is represented as follows:

- Instances used in

p 3 2 e 1 2 e 2 3

- directed graphs
- directed random graphs.
- For instance, 3 nodes graph whose arcs are \((1, 2),(3, 2)\) is represented as follows:

p 3 2 e 1 2 e 3 2