DTAI

Monday, May 7 2012, at 16h30 in Celestijnenlaan 200A (auditorium 00.225)

An approximative method for solving ∃∀ satisfiability problems
by Hanne Vlaeminck (PhD student DTAI)

Many interesting problems, such as conformant planning, i.e., planning problems where the initial situation is not completely known, can be naturally expressed as finite domain satisfiability problems of the fragment ∃∀SO of second-order logic. Such satisfiability problems are computationally hard and many of these problems are often solved approximately.

In this talk, I will start from a concrete conformant planning problem and use this to illustrate that this is indeed an ∃∀SO satisfiability problem, and provide intuitions about how one can approximately solve such a conformant planning problem. The key in this is the use of a syntactic representation of a constraint propagation method for first- order logic. By using this syntactic
representation, we can transform a conformant planning into a standard planning problem, in a sound but incomplete way, which can be handled by existing solvers.

Next, I will show how this approximation method is not specific to conformant planning problems but can be generalized to approximate any ∃∀SO(ID) satisfiability problem. This gives us a general theoretical framework for a number of approximative methods in the literature.