Declarative Problem Solving
Many efforts have been spent to develop problem solving methods in which solutions are described in terms of desired properties (i.e., how a solution looks like) rather than computing them by means of an explicit algorithm. Our work on this currently centers around Answer Set Programming, which is a recent problem solving paradigm, but also addresses declarative planning and applying SAT and QSAT solvers for solving advanced reasoning tasks more quickly. Furthermore, we are interested in language extensions which allow for a more user-friendly and compact problem formalization.
Answer Set Programming
Answer Set Programming (ASP) is a popular, purely declarative, problem solving formalism. ASP allows for the encoding of problems in a succinct way. Such a problem encoding usually consists of a set of rules representing the underlying constraints of the problem and sets of facts describing concrete scenarios. The solutions are given in terms of answer sets, which capture the evaluation of the rules. In our group, we study the foundation of ASP as a formalism as well as its application in several domains, like scheduling, planning, reasoning problems, and other combinatorial problems arising from industry.
(Q)SAT Solving
SAT solving refers to finding satisfying assignments to a given propositional formula and while it is one of the oldest declarative problem solving formalism, it has not lost any of its relevance today. Simply by translating a given problem into SAT, solutions can be found quickly and effectively. Quantified SAT (QSAT) is an extension of SAT where we also allow quantification over the truth-values of the variables, enabling as to represent and solve even more complex problems, like abductive reasoning.
Hybrid Methods
While the above mentioned problem solving approaches are powerful, they can often be enhanced by by interleaving them with incomplete solving techniques like local search or decomposition approaches. This is especially the case when trying to solve industrial scale optimization problems. For example, one can, starting from an initial solution, iteratively destroy parts of the incumbent solution and repair it using ASP or (QSAT) such the the newly obtained solution is of better quality. This is known as Large Neighborhood Search. Designing and applying such and similar hybrid methods are ongoing topics of research in our group.