SAT Compilation for Constraints over Structured Finite Domains

Datum

07.02.2017

Zeit

10:00 - 11:00

Sprecher

Dipl.-Inf. (FH) Alexander Bau

Zugehörigkeit

Institut für Theoretische Informatik, Grundlagen der Programmierung

Sprache

en

Hauptthema

Informatik

Andere Themen

Informatik

Beschreibung

A constraint is a formula in first-order logic expressing a relation between values over various domains. In order to solve such a constraint, constructing a propositional encoding is a successfully applied technique. These encodings are often created by a problemspecific generator program or by crafting them manually. The present thesis introduces the constraint solver CO4 that automatically generates propositional encodings for constraints over finite structured domains written in a syntactical subset of the functional programming language Haskell. This subset of Haskell enables the specification of expressive and concise constraints by supporting user-defined algebraic data types, pattern matching, and recursive functions, as well as higher-order and polymorphic types. After an external SAT solver determined a satisfying assignment for the variables in the generated propositional encoding, a solution in the domain of discourse is derived without user interaction. This approach is even applicable for finite restrictions of recursively defined algebraic data types, which, in general, entail an infinite set of values. The present thesis describes all aspects of CO4 in detail: the language used for specifying constraints, the solving process, and its correctness, as well as applications where CO4 has been applied.

Letztmalig verändert: 07.02.2017, 08:48:29