Answer Set Programming with Clause Learning

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 been very important in improving the efficiency of satisfiability (SAT) solvers over the past few years, especially on structured problems coming from applications. We describe how we have adapted conflict clause techniques for use in the answer set solver Smodels. We experimentally compare the resulting program to the original Smodels program. We also compare to ASSAT and Cmodels, which take a different approach to adding clauses to constrain an answer set search.

• Type: Conference
• Year: 2004
• Where: LPNMR
• Authors: Jeffrey Ward, John S. Schlipf
• Keywords: Answer Set, Backtracking Solver Analysis, Conflict Clause, LPNMR 2004