Overview

BOB is a SAT-based tool for constructing optimal linear layouts of graphs. With a modern SAT solver, it is capable to compute optimal stack, queue, or track layouts of graphs with hundreds of vertices within several minutes.

Visit https://spupyrev.github.io/linearlayouts.html for a survey of existing results regarding upper and lower bounds on stack number, queue number and track number of various classes of graphs. If you use BOB in your research, please cite it as follows:

@misc{bob,
  author       = {Pupyrev, Sergey},
  title        = {A {SAT}-based solver for constructing optimal linear layouts of graphs},
  howpublished = {\url{https://github.com/spupyrev/bob}},
  year         = {2017},
  note         = {Accessed: today's date}
}

Basic Setup

1. Compile the library by running:

    make
   

2. Run the tool:

    bob -i=graphs/graph.dot -o=graph.dimacs -stacks=3
   

   The tool accepts graphs in the DOT and GML formats. The output is the DIMACS format. For the list of supported options use:

    bob -help
   

3. Download and setup a SAT solver such as Lingeling or Glucose

4. Use the SAT solver to test embeddability of the graph:

    treengeling graph.dimacs > result.dimacs
   

5. Print the resulting layout:

    bob -i=graphs/graph.dot -result=result.dimacs -stacks=3
   

Examples

Test whether an input graph can be embedded in 2 stacks

    bob -i=graphs/graph.dot -o=graph.dimacs -stacks=2

Test whether an input graph can be embedded in 2 queues

    bob -i=graphs/graph.dot -o=graph.dimacs -queues=2

Test whether an input graph admits a 6-track layout and print resulting layout

    bob -i=graphs/weakly_6tracks.gml -o=graph.dimacs -tracks=6
    treengeling graph.dimacs > result.dimacs
    bob -i=graphs/weakly_6tracks.gml -result=result.dimacs -tracks=6

License

Code is released under the MIT License.