Graph Drawing using SAT (GDSAT)

In a grid-based representation of a graph, vertices and edges correspond to axis-parallel boxes on an underlying integer grid. Boxes can be further constrained in their shapes and interactions by additional problem-specific constraints. Our framework GDSAT defines a generic SAT model that is flexible enough to capture a large variety of different grid-based graph layout problems, both polynomially-solvable and NP-complete. The dimension of the grid is not restricted.

Currently, we have implemented instantiations for six different NP-complete example problems:

• pathwidth
• bandwidth
• optimum st-orientation
• minimum area bar visibility representation
• minimum area bar k-visibility representation
• boxicity-k testing

These instantiations have been tested on the well-known Rome graphs in our paper [1].

Of course the flexibility of GDSAT comes at the cost of losing some of the efficiency of more specific approaches. The goal of this framework, however, is not to achieve maximal performance for a specific problem, but to provide an easy-to-adapt solution method for a large class of graph representation problems, which allows quick and simple prototyping for instances that are not too large.

More information about the theoretical background and experiments applied on the framework is given in [1].

gdsat.

The framework GDSAT is written in C++ and makes use of the SAT solver MiniSat, which can be downloaded at http://minisat.se/.

This framework is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. Further, this framework is distributed in the hope that it will be useful, but without any warranty; without even the implied warranty of merchantibility or fitness for a particular purpose. See the GNU General Public License for more details.

In case of questions please contact Benjamin Niedermann.