Research Project: G12 Constraint Programming Platform
|
|
NICTA's G12 project, which ran from 2005 until 2010, aimed to
develop a new constraint programming platform featuring a suite
of languages. Traditionally, the main application area for
constraint solving technology is scheduling, but the platform is
suitable for a vast range of other applications, ranging from
computing layouts and other designs to discrete event monitoring
and control.
Zinc is a modelling language based on first order logic
with extensions to accommodate numerical constraints and
commonly used data structures such as arrays, sets and
records. It allows the model or generic domain
description to be separated from the data or specifics of
the problem instance, and crucially allows problem modelling to
be solver-independent. We may think of the process of solving
the problem as one of evaluating the Zinc model and data,
as logically what it amounts to is finding an interpretation of
the language on which all of the constraints come out true.
Mercury is the logic programming language of that name,
used in G12 as a basis for constraint logic programming on top
of solvers drawn from the OR and CP/SAT communities. It allows
solvers of different kinds, say a MIP solver, a local search
solver and a SAT solver, to be combined into hybrids suitable
for a particular problem. Some of the solvers are native to the
platform. Others are by third party software providers and are
able to work within G12 via a simple and flexible API.
Between Zinc and Mercury (remember your periodic table)
comes Cadmium, a language for specifying syntactic
transformations. It is used to transform Zinc models into
simpler ones, for instance by reifying constraints and
flattening the result. It is also intended for specifying the
mapping from Zinc models into Mercury programs that solve them.
My part in all this was to head the part of the work being done
in Canberra, in close collaboration with the principal team in Melbourne, and others in
Sydney and Brisbane. In Canberra, we worked on SAT solvers, on
incorporating first order theorem provers into the software for
analysing Zinc models, on the first version of the integrated development environment
which formed the front end for the G12 user, and
on a range of visualisation tools.
|
The G12 platform forms the basis of software now commercialised by the Melbourne-based company
Opturion. Alas, our IDE is no longer current, but
our research on constraint visualisation resulted at the very least in some striking
images, and remains an interest of mine on the personal research level.
The images on this page were produced by the G12 visualisation
toolkit as it was around 2010. They show static views of constraint graphs revealing the
structure of SAT-like realisations of problems in AI planning and
bounded model checking. Each vertex is a variable, and two variables
are joined by an edge if they co-occur in at least one
constraint. The constraint graph viewer in G12 used a quasi-physical
force-directed layout: imagine that all vertices repel each other
like similarly charged particles, with a force that obeys an inverse
square law, and that edges pull adjacent vertices together with a
force linear in the length of the edge, like springs with a rest
length of zero. While the examples shown here are 2-dimensional, so
as to show a maximum of vertices without overlap, in some cases 3D
layouts are also also useful and intuitive.
For more on G12 and the visualisation sub-project, click
here and
here.
Dr J K Slaney Phone (Aus.): (026) 125 8607
Automated Reasoning Project Phone (Int.): +61 26 125 8607
Australian National University Fax (Aus.): (026) 125 8651
Canberra, ACT, 0200, AUSTRALIA Fax (Int.): +61 26 125 8651
John.Slaney@anu.edu.au
|
