Monday April 30, 2012, at 16h30 in Celestijnenlaan 200A (auditorium 00.225)
Constraint Programming support for IDP
by Stef De Pooter (PhD student DTAI)
One state-of-the-art method for generating solutions to problems modeled in logic languages such as first-order logic, FO(.) and ASP, is the so-called "ground-and-solve" approach. In the first phase, the theory is combined with the input structure and transformed into an (almost) propositional format. In the second phase, a SAT solver searches for models of the transformed theory.
However, when problem at hand has (very) large domains -- which is often the case in practice, e.g. long-term scheduling, calculations in accountancy, ... -- the size of the grounding becomes intractable and the solver will never get to the searching part. One way to take on this problem is to make use of techniques from Constraint Programming (CP), where efficient non-ground propagation algorithms are available for specific types of constraints.
In this talk I will show how we are modifying the grounding algorithm to recognize those constraints and instead of grounding them, use a CP solver as backend to handle propagation over them. This way we are combining strengths of SAT and CP. The SAT solver is in charge of making decisions, and the CP solver offers support for satisfying constraints over large domains.