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

  1. Download the latest version.
  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

Download

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

Author: Takehide Soh

Created: 2015-01-13 火 10:22

Emacs 24.3.1 (Org mode 8.2.8)

Validate