Logic-based tools for modeling and solving combinatorial problems

Master Specialization: Algorithms and Programming
Topic Aproval date: 18/02/09
Orientation: research

Student: Miquel Palahí.
Thesis advisor(s): Miquel Bofill i Mateu Villaret.
Contact:

The framework of this Master Thesis is the application of logic based methods and tools to the modeling and resolution of combinatorial problems. These combinatorial problems arise in quotidian life through scheduling, timetabling, resource allocation, etc. The main goal of this thesis are the study and design of a declarative programming language for modeling combinatorial problems, and the development of a compiler for such a language that generates SAT modulo theories (SMT) formulae, i.e. boolean formulae enriched with first-order theories like the diference logic, the linear integer arithmetic, etc. The expressivity of SMT, together with the efficiency of the recent developed tools for solving these satisfiability problems, gives to this project the warranty and the innovative feeling needed for a Master Thesis.