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