VL Constraint-Programmierung

Constraints gibt es überall: die meisten algorithmischen Aufgabenstellungen bestehen aus Einschränkungen an eine Menge von möglichen Lösungen. Die Constraint-Programmierung ist eine Technik zur Lösung solcher Aufgaben, bei der Formulierungen solcher Einschränkungen Bestandteile von Programmen sind. In der Praxis wird Constraint-Programmierung zum Schließen mit unvollständigem Wissen, zum Lösen kombinatorischer Probleme, zur Modellierung, Simulation und Diagnose und in vielen anderen Bereichen industriell angewendet. (Quelle: Hofstedt/Wolf 2007)

Literatur:

• Krzysztof Apt: Principles of Constraint Programming, Cambridge Univ. Press
• Daniel Kroening and Ofer Strichman: Decision Procedures, Springer 2008.
• Petra Hofstedt und Armin Wolf: Einführung in die Constraint-Programmierung, Springer 2007.
• Alexander Bau: SAT Compilation for Constraints over Structured Finite Domains, Dissertation, TU Dresden 2017

Software (Auswahl):

• Niklas Een, Niklas Sörensson: Minisat
• Niklas Björner, Leonardo de Moura, Lev Nachmanson, Christoph Wintersteiger: Programming Z3
• Edward A. Kmett et al. A Monad for expressing SAT or QSAT problems using Observable Sharing
• Christian Schulte, Guido Tack, Mikael Z. Lagerkvist: Modeling and Programming with Gecode
• Boolean Satisfiability: SAT Competitions
• Satisfiability Modulo Theories: SMT-COMP