SAT-based answer set programming

dc.contributor.advisorLifschitz, Vladimiren
dc.contributor.committeeMemberBoyer, Roberten
dc.contributor.committeeMemberGal, Annaen
dc.contributor.committeeMemberStone, Peteren
dc.contributor.committeeMemberTruszczynski, Miroslawen
dc.creatorLierler, Yuliyaen
dc.date.accessioned2010-09-29T21:40:58Zen
dc.date.available2010-09-29T21:40:58Zen
dc.date.available2010-09-29T21:41:04Zen
dc.date.issued2010-05en
dc.date.submittedMay 2010en
dc.date.updated2010-09-29T21:41:05Zen
dc.descriptiontexten
dc.description.abstractAnswer 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.en
dc.description.departmentComputer Sciences
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttp://hdl.handle.net/2152/ETD-UT-2010-05-888en
dc.language.isoengen
dc.subjectAnswer set programmingen
dc.subjectLogic programmingen
dc.subjectPropositional satisfiabilityen
dc.subjectAnswer set solversen
dc.subjectSATen
dc.subjectSAT solversen
dc.subjectSmodelsen
dc.subjectCmodelsen
dc.titleSAT-based answer set programmingen
dc.type.genrethesisen
thesis.degree.departmentComputer Sciencesen
thesis.degree.disciplineComputer Sciencesen
thesis.degree.grantorUniversity of Texas at Austinen
thesis.degree.levelDoctoralen
thesis.degree.nameDoctor of Philosophyen
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
LIERLER-DISSERTATION.pdf
Size:
926.1 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
2.12 KB
Format:
Plain Text
Description: