|
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.
|
