Efficient SAT-based answer set solver

Show full item record

Title: Efficient SAT-based answer set solver
Author: Lin, Zhijun
Abstract: Recent research shows that SAT (propositional satisfiability ) techniques can be employed to build efficient systems to compute answer sets for logic programs . ASSAT and CMODELS are two well -known such systems that work on normal logic programs . They find an answer set from the full models for the completion of the input program , which is (iteratively ) augmented with loop formulas . Making use of the fact that , for non -tight programs , during the model generation , a partial assignment may be extensible to a full model but may not grow into any answer set , we propose to add answer set extensibility checking on partial assignments . Furthermore , given a partial assignment , we identify a class of loop formulas that are "active'' on the assignment . These "active'' formulas can be used to prune the search space . We also provide an efficient method to generate these formulas . These ideas can be implemented with a moderate modification on SAT solvers . We have developed a new answer set solver SAG on top of the SAT solver MCHAFF . Empirical studies on well -known benchmarks show that in most cases it is faster than the state -of -the -art answer set solvers , often by an order of magnitude . For disjunctive logic programs , the existing SAT -based solvers translate them into propositional formulas based on a complex completion definition , and then make use of loop formulas and SAT solvers to find answer set . In this paper we present a new approach that allows the translation of a program into a formula that is weaker but less complex than the completion . It performs answer set checking on partial assignments . In case a partial assignment is inextensible to an answer set , we use support formulas , which is a generalization of loop formula , to prevent the repetition of the same mistake . Empirical studies on disjunctive logic programs confirm the performance advantage of the new approach .
URI: http : / /hdl .handle .net /2346 /20592
Date: 2007-12


Efficient SAT-based answer set solver. Doctoral dissertation, Texas Tech University. Available electronically from http : / /hdl .handle .net /2346 /20592 .

Files in this item

Files Size Format View
Lin_Zhijun_Diss.pdf 339.9Kb application/pdf View/Open

This item appears in the following Collection(s)

Show full item record

Search DSpace

Advanced Search