# hss: HCP Solver based on Scarab and Sat4j

## Overview

This page details Hamiltonian Cycle Problem Solver "hss" which is based on Scarab and Sat4j.

### Requirements

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

### How to use it

2. Edit file "hss" for your environment.
3. 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


### 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

• 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:
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