Between constraints and satisfaction

Oliver Kullmann


I want to give an overview on the more practical aspects of my current work: Developing
new algorithms and frameworks for hard constraint satisfaction and satisfiability problems,
and implementing a generative (C++) library (the OKlibrary) based on these ideas.
The algorithmic ideas will be explained using easy examples, for example Sudoku
problems (which are interesting when they are bigger).

The title should be more accurately ``Between constraints and satisfiability'', where
``constraints'' refers to the world of constraint satisfaction, with its emphasise on modularity
and a (certain degree of) abstraction, while ``satisfiability'' refers to be world of (boolean)
satisfiability problems, with its emphasise on algorithms, complexity and implementations.
One of the main goals of the new algorithmic framework is to unify these two worlds, based
on new concepts of ``generalised satisfiability problems''.

These ideas are developed in strong interaction with the development of the OKlibrary, which
is a generic library (strongly based on abstract data types) and also a generative library (the
library is not static, but has a lot of computational power to be flexible and adaptive). One
of the main novelties here (purely on the software engineering side) is a framework for
``higher order unit testing'', which fully integrates unit testing into a generic library.
Tuesday 12th December 2006, 14:00
Robert Recorde Room
Department of Computer Science