SAT Compilation for Constraints over Structured Finite Domains

Date

Feb 7, 2017

Time

10:00 AM - 11:00 AM

Speaker

Dipl.-Inf. (FH) Alexander Bau

Affiliation

Institut für Theoretische Informatik, Grundlagen der Programmierung

Language

en

Main Topic

Informatik

Other Topics

Informatik

Description

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.

Last modified: Feb 7, 2017, 8:48:29 AM