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

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

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 paper in DOI.
- 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

Links

Scarab	SAT-based CP System
Sat4j	SAT solver in Java, which Scarab adopts!