The G12 project aims to allow one to model a combinatorial optimization problem in a high level way, independent of the solving technology that you will use to solve it. The model is then transformed to a low level model that can be executed by a constraint solver. The same model can be transformed to use finite domain constraint solving, mixed integer linear programming, Boolean satisfaibility (SAT) solving, local search (e.g. simulated annealing) as well as hybrid of the different approaches.

The requirement to efficiently transform high level models lead us to develop Cadmium a AC term rewriting language, which treats conjunction specially. So called ACD term rewriting allows one to refer in a rewrite rule to all the constraints that hold in the context of the term being rewritten. This allows one to write very concise and transparent code for rewriting logical formulae. This power of ACD term rewriting is unsurprisingly the hard part to implement efficiently.

In the talk I will briefly talk about G12 and the introduce Cadmium, before talking about how to implement ACD term rewriting, and point out where we still need to improve the implementation of Cadmium.