Title: | SAT-based answer set programming |

Author: | Lierler, Yuliya |

Abstract: | Answer set programming (ASP ) is a declarative programming paradigm oriented towards difficult combinatorial search problems . Syntactically , ASP programs look like Prolog programs , but solutions are represented in ASP by sets of atoms , and not by substitutions , as in Prolog . Answer set systems , such as Smodels , Smodelscc , and DLV , compute answer sets of a given program in the sense of the answer set (stable model ) semantics . This is different from the functionality of Prolog systems , which determine when a given query is true relative to a given logic program . ASP has been applied to many areas of science and technology , from the design of a decision support system for the Space Shuttle to graph -theoretic problems arising in zoology and linguistics . The "native" answer set systems mentioned above are based on specialized search procedures . Usually these procedures are described fairly informally with the use of pseudocode . We propose an alternative approach to describing algorithms of answer set solvers . In this approach we specify what "states of computation" are , and which transitions between states are allowed . In this way , we define a directed graph such that every execution of a procedure corresponds to a path in this graph . This allows us to model algorithms of answer set solvers by a mathematically simple and elegant object , graph , rather than a collection of pseudocode statements . We use this abstract framework to describe and prove the correctness of the answer set solver Smodels , and also of Smodelscc , which enhances the former using learning and backjumping techniques . Answer sets of a tight program can be found by running a SAT solver on the program's completion , because for such a program answer sets are in a one -to -one correspondence with models of completion . SAT is one of the most widely studied problems in computational logic , and many efficient SAT procedures were developed over the last decade . Using SAT solvers for computing answer sets allows us to take advantage of the advances in the SAT area . For a nontight program it is still the case that each answer set corresponds to a model of program's completion but not vice versa . We show how to modify the search method typically used in SAT solvers to allow testing models of completion and employ learning to utilize testing information to guide the search . We develop a new SAT -based answer set solver , called Cmodels , based on this idea . We develop an abstract graph based framework for describing SAT -based answer set solvers and use it to represent the Cmodels algorithm and to demonstrate its correctness . Such representations allow us to better understand similarities and differences between native and SAT -based answer set solvers . We formally compare the Smodels algorithm with a variant of the Cmodels algorithm without learning . Abstract frameworks for describing native and SAT -based answer set solvers facilitate the development of new systems . We propose and implement the answer set solver called SUP that can be seen as a combination of computational ideas behind Cmodels and Smodels . Like Cmodels , solver SUP operates by computing a sequence of models of completion of the given program , but it does not form the completion . Instead , SUP runs the Atleast algorithm , one of the main building blocks of the Smodels procedure . Both systems Cmodels and SUP , developed in this dissertation , proved to be competitive answer set programming systems . |

URI: | http : / /hdl .handle .net /2152 /ETD -UT -2010 -05 -888 |

Date: | 2010-09-29 |

Files | Size | Format | View |
---|---|---|---|

There are no files associated with this item. |