Lecture notes in computer science vol:4790 pages:378-392
Logic for Programming, Artificial Intelligence, and Reasoning location:Yerevan, Armenia date:October 16-19, 2007
We investigate techniques for supporting inductive definitions (IDs) in SAT, and report on an implementation, called MidL, of the resulting solver. This solver was first introduced in [Marien et al. 2006], as a part of a declarative problem solving framework. We go about our investigation by proposing a new formulation of the semantics of IDs as presented in [Denecker 2000]. This new formulation suggests a way to perform the computational task involved, resulting in an algorithm supporting IDs. We show in detail how to integrate our algorithm with traditional SAT solving techniques. We also point out the similarities with another algorithm that was recently developed for ASP [Anger et al. 2006]. Indeed, our formulation reveals a very tight relation with stable model semantics. We conclude by an experimental validation of our approach using MidL.