D-FLAT is a framework that allows you to specify dynamic programming algorithms that work on a tree decomposition in a declarative way by means of Answer Set Programming (ASP).
A detailed description of the system is given in our [Technical Report DBAI-TR-2014-86, Technische Universität Wien, 2014] (http://dbai.tuwien.ac.at/research/report/dbai-tr-2014-86.pdf).
Please see our [project page] (http://dbai.tuwien.ac.at/research/project/dflat/) for more information.
For instructions about compiling D-FLAT, please read the INSTALL file.
For getting a usage message that describes the invocation of D-FLAT and all command-line options, use the help option:
An example invocation of D-FLAT for solving the 3-Colorability problem on a
graph specified in the file
dflat -p applications/graph_problems/3col/dynamic.lp -f instance.lp
Depending on the graph, this may produce the following output.
Solutions: ┣━ map(0,red) map(1,green) map(2,blue) map(3,red) ┣━ map(0,red) map(1,blue) map(2,green) map(3,red) ┣━ map(0,green) map(1,red) map(2,blue) map(3,green) ┣━ map(0,blue) map(1,red) map(2,green) map(3,blue) ┣━ map(0,green) map(1,blue) map(2,red) map(3,green) ┗━ map(0,blue) map(1,green) map(2,red) map(3,blue)
The first line of the 3-Colorability encoding contains the following modeline.
%dflat: --tables -e vertex -e edge
A modeline such as this one has the effect of automatically adding the string
after the colon to the command-line arguments. It should contain arguments
without which running the encoding does not make sense. In this case,
--tables is used to tell D-FLAT's ASP solving module to use predicates like
childRow/2 to describe a table for each tree decomposition node. The two
-e specify that in the input graph (
instance.lp in this
case) the respective predicates denote (hyper-)edges. (
vertex is supplied
because isolated vertices would otherwise not be included in the tree
As a further example, if it suffices to just count the number of solutions
without enumerating them, we can use the option
--depth 0. Solutions (and
candidates for solutions) are represented in D-FLAT using so-called item
trees. For the 3-Colorability encoding, such an item tree always has an empty
root, and the children of this root represent the solution candidates.
--depth i has the effect that when D-FLAT has finished computing
the item tree at each decomposition node only item tree nodes up to level i are
materialized. In this case, only the (empty) root of the item tree of solutions
is materialized. Furthermore, the number of child nodes that have thus been
omitted is printed. For 3-Colorability, this number therefore amounts to the
number of solutions. The following is the output for the same input graph when
--depth 0 is added.
For monitoring what is going on during the computation, it is often useful to
print the generated decomposition using the option
Human-readable debugging output can be generated using the option