Development of a tool to solve mixed logical/linear constraint problems (bibtex)
by Michael Tautschnig
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.\par 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.\par 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.\par 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.
Reference:
Development of a tool to solve mixed logical/linear constraint problemsMichael TautschnigFebruary 2006, Master's thesis, Technische Universität München.
Bibtex Entry:
@mastersthesis{tautschnig:diploma06,
  author = {Michael Tautschnig},
  title = {Development of a tool to solve mixed logical/linear constraint problems},
  month = {February},
  year = {2006},
  school = {Technische Universit{\"a}t M{\"u}nchen},
  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.\par

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

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

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.}
}
Powered by bibtexbrowser