Reference:

Michael Tautschnig. Development of a tool to solve mixed logical/linear constraint problems. Master's thesis, Technische Universität München, February 2006.

Abstract:

The problem of solving mixed arithmetic and Boolean constraint systems arises in many different areas, such as verification of soft- and hardware systems, resource planning or system design and has been studied extensively in recent time. Yet, the available solvers are neither easily extensible, nor do they offer ways to apply problem specific heuristics that are required for most of the hard problems in this area.

To overcome these limitations, a framework has been designed to integrate state-of-the-art solvers for the Boolean- and parts of the arithmetic domain to solve the combined problem. Thereby we benefit from the full strength of each of the tools in their special area. Furthermore, the architecture of the system emphasises extensibility, which already proved useful for the implemented extension to non-linear arithmetic constraints.

The results show that our implementation, albeit in in some parts not yet more than a proof of concept, can already compete with existing solvers. Due to the extension to non-linear arithmetic we are even able to tackle a new class of real-world problems.

The present work introduces this class of problems and our approach to solve them, accompanied by some real-life examples. Along with these descriptions we provide detailed insight into our tool and the hurdles we had to overcome.

Suggested BibTeX entry:

@mastersthesis{tautschnig:diploma06,
    author = {Michael Tautschnig},
    month = {February},
    school = {Technische Universit{\"a}t M{\"u}nchen},
    title = {Development of a tool to solve mixed logical/linear constraint problems},
    year = {2006}
}