Title: Integrating inductive definitions in SAT
Authors: MariĆ«n, Maarten ×
Wittocx, Johan
Denecker, Marc #
Issue Date: Oct-2007
Publisher: Springer
Series Title: Lecture notes in computer science vol:4790 pages:378-392
Conference: Logic for Programming, Artificial Intelligence, and Reasoning location:Yerevan, Armenia date:October 16-19, 2007
Abstract: 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.
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Status SizeFormat
lpar07.pdf Accepted 266KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science