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.