Abstract. The structure of a CSP (and of related problems such as e.g. conjunctive database queries is best described by a hypergraph. It is well-known that in case this hypergraph is acyclic, the CSP can be solved efficiently. In this talk various methods of generalizing the notion of hypergraph acyclicity will be discussed. In particular, we will introduce the audience into the method of "Hypertree Decompositions" developed at TU Wien. Hypergraph decomposition methods can be used, in particular, to simplify diagnostic problems.
Abstract. In recent years, there has been an explosion of research in AI into propositional satisfiability (or SAT). There are many factors behind the increased interest in this area. One factor is the improvement in search procedures for SAT. New local search procedures are able to solve SAT problems with thousands of variables. At the same time, implementations of complete search algorithms like Davis-Putnam have been able to solve open mathematical problems. Another factor is the identification of hard SAT problems at a phase transition in solubility. A third factor is the demonstration that we can often solve real world problems by encoding them into SAT. This talk reviews the state of the art for research into satisfiability , and discuss applications like model checking in which algorithms for satisfiability have proved successful.
Abstract. Every programmer has seen this before: A program does not run as it is supposed to be. To fix the failure, one must narrow down the possible failure causes. This narrowing is typically a manual task, dependent on the skill and the endurance of the programmer. In this talk, we shall present some techniques that widely automate the quest for failure causes. Based on a simple trial-and-error process and an automated test, it is fairly simple to isolate external failure causes like input, code differences, or thread schedules. Advanced techniques can even isolate causes and effects within the program run: "First, variable x_1 had a value of x_1, thus v_2 became x_2, thus v_3 was set to x_3 ... and thus the program failed". Case studies on real programs with real bugs, from Mozilla to the GNU C compiler, demonstrate the practical feasability of these experimental approaches.