TexasScholarWorks
    • Login
    • Submit
    View Item 
    •   Repository Home
    • UT Electronic Theses and Dissertations
    • UT Electronic Theses and Dissertations
    • View Item
    • Repository Home
    • UT Electronic Theses and Dissertations
    • UT Electronic Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    SAT-based answer set programming

    Thumbnail
    View/Open
    LIERLER-DISSERTATION.pdf (926.1Kb)
    Date
    2010-05
    Author
    Lierler, Yuliya
    Share
     Facebook
     Twitter
     LinkedIn
    Metadata
    Show full item record
    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.
    Department
    Computer Sciences
    Description
    text
    Subject
    Answer set programming
    Logic programming
    Propositional satisfiability
    Answer set solvers
    SAT
    SAT solvers
    Smodels
    Cmodels
    URI
    http://hdl.handle.net/2152/ETD-UT-2010-05-888
    Collections
    • UT Electronic Theses and Dissertations

    University of Texas at Austin Libraries
    • facebook
    • twitter
    • instagram
    • youtube
    • CONTACT US
    • MAPS & DIRECTIONS
    • JOB OPPORTUNITIES
    • UT Austin Home
    • Emergency Information
    • Site Policies
    • Web Accessibility Policy
    • Web Privacy Policy
    • Adobe Reader
    Subscribe to our NewsletterGive to the Libraries

    © The University of Texas at Austin

     

     

    Browse

    Entire RepositoryCommunities & CollectionsDate IssuedAuthorsTitlesSubjectsDepartmentsThis CollectionDate IssuedAuthorsTitlesSubjectsDepartments

    My Account

    Login

    Statistics

    View Usage Statistics

    Information

    About Contact Policies Getting Started Glossary Help FAQs

    University of Texas at Austin Libraries
    • facebook
    • twitter
    • instagram
    • youtube
    • CONTACT US
    • MAPS & DIRECTIONS
    • JOB OPPORTUNITIES
    • UT Austin Home
    • Emergency Information
    • Site Policies
    • Web Accessibility Policy
    • Web Privacy Policy
    • Adobe Reader
    Subscribe to our NewsletterGive to the Libraries

    © The University of Texas at Austin