Research Project: G12 Constraint Programming Platform
|
|
NICTA's G12 project, scheduled to conclude in 2010, aims 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 is to head the part of the work being done
in Canberra, in close collaboration with the teams in Melbourne,
Sydney and Brisbane. Here we are working on SAT solvers, on
incorporating first order theorem provers into the software for
analysing Zinc models, on the integrated development environment
which will eventually form the front end for the G12 user, and
on a range of visualisation tools.
|
The images on this page are produced by the G12 visualisation
toolkit. 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 uses a quasi-physical
force-directed layout: we 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 about the G12 project,
click here.
G12 Slogans
-
STRP: Solve The Real
Problem
-
Too often, the first step in addressing a problem is to simplify
it by stripping away the ugly details that don't fit the modelling
language or solving paradigm. Unfortunately, this means that the
problem you solve is not the one the client has. Enrich your
language and toolkit until you can express the problem, and strive
to solve it, warts and all.
-
DHS: Don't Hammer Screws
-
Use the right tool for the job, or the job will be botched. If
you don't have the right tool, expand your toolkit. Learn the
correct use of all your tools, and seek ways to select and
combine them to the best effect.
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
|
