149. Informatik-Kolloquium
Vortrag im Rahmen des Forschungsseminars der Professur Modellierung und Simulation
Prof. Christian Posthoff
University of the West Indies,Trinidad & Tobago
"Constraint Programming Based on Logic Equations"
Donnerstag, 09.07.2009
15:30 Uhr, 1/336
Alle interessierten Personen sind herzlich eingeladen!
Abstract:
It is well known and state of the art that many problems in Artificial Intelligence, Discrete Mathematics, Combinatorics, Graph Theory … can be modeled by means of Logic Equations and particularly by means of conjunctive forms (constraints). The satisfiability or unsatisfiability of these forms and the complexity of the solution algorithms are very interesting problems known as SAT-problem.Up to now the use of "Ordered Binary Decision Trees (OBDT)" and resolution-based algorithms were the dominating concepts for the solution of different problems (very often restricted to special cases, conditions or questions).
This paper shows the use of ternary vectors" as an efficient new data structure for these problems. Even if it is "only" a new data structure, many advantages can be seen and confirmed by applications from many different fields:
" The modeling process is easy to understand, very flexible and can be adapted to many areas, based on the efficient data structure.
" The processing of the ternary vectors can be implemented fully in parallel on different hard- and software levels and platforms.
" The solution algorithms always find all solutions (no solution, one solution, many solutions) without special considerations.
Examples from Graph Theory (node bases, Eulerian paths, Hamiltonian circuits, 4-colour-problems, …), games (Sudoku, chess), SAT-problem questions (minimal unsatisfiable and maximal satisfiable sets of disjunctions in a conjunctive form, …) show the elegance and the efficiency of this data structure and the algorithms that can be built on this foundation.
