These graphs show three views of the same thing: the constraint
structure of a MiniZinc model which takes as data a set of
tables representing an algebraic structure suitable for
modelling propositional logic, and determines which if any of a
collection of distributive substructural logics it
satisfies. Thus this application uses G12 for what is in a sense
the inverse of the problem solved by
MaGIC.
In the top constraint graph, the nodes are as usual the decision
variables, and the edges join variables related by
constraints. The colours of vertices represent the arrays of
which they are elements, with non-array variables coloured in
the default orange-grey.
The middle graph is roughly the inverse of the top one: the
vertices are the constraints, and an edge joins two constraints
if they have a variable in common.
Lastly, the bottom graph shows the bipartite view. Round nodes
are variables, triangular ones are constraints, and the edges
join variables to the constraints in which they occur.
Click on the images to see them at full size.
Very few of the decision variables in this CSP are actually
specified in the Zinc model. The rest are introduced in order to
reify constraints and the like when the high-level model is
automatically transformed into a low-level one. The clusters of
vertices that look like eyes are cliques in the constraint
graph. This problem is actually very easy for the solver, as
once it has fixed a few values the results propagate everywhere
to give either a solution or a very shallow backtrack.
|