In this dissertation we show how conflict clause learning, a technique that has been very useful in improving the efficiency of Boolean logic satisfiability search, can be adapted to speed up dramatically the search for models of answer set programs.
Answer set programming is a knowledge representation paradigm related to the areas of logic programming and nonmonotonic reasoning. Many of the applications of answer set programming come from the areas of artificial intelligence – related diagnosis and planning. The problem of finding an answer set for a normal or extended logic program is NP-hard. Current complete answer set solvers are patterned after the Davis-Putnam-Loveland-Logemann (DPLL) algorithm for solving Boolean satisfiability (SAT) problems, but are adapted to the nonmonotonic semantics of answer set programming.
Recent SAT solvers include improvements to the DPLL algorithm. Conflict clause learning has been particularly effective in this regard. A conflict clause represents a backtracking solver's analysis of why a conflict occurred. This analysis can be used to further prune the search space and to direct the search heuristic. The use of such clauses has improved significantly the efficiency of satisfiability solvers over the past few years, especially on structured problems arising from applications.
In this dissertation we describe how we have adapted conflict clause techniques for use in the answer set solver Smodels . We experimentally compare the performance of the resulting program, Smodels cc, to that of the original Smodels program. Our tests show dramatic speedups for Smodelscc on a wide range of problems.
We also compare the performance of Smodelscc with that of two other recent answer set solvers, ASSAT and Cmodels-2. ASSAT and Cmodels-2 directly call Boolean satisfiability solvers in order to search for answer sets. On so-called “non-tight” problems, Smodelscc showed substantially better performance than these solvers. The performance advantage that Smodelscc enjoys on non-tight problems is due to the unfounded set test that Smodelscc inherits from the Smodels solver, and the fact that this test is executed frequently throughout the program's search for answer sets.