Fast SAT-based Answer Set Solver

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. 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 S...

• Type: Conference
• Year: 2006
• Where: AAAI
• Authors: Zhijun Lin, Yuanlin Zhang, Hector Hernandez
• Keywords: AAAI 2006, Answer Set, Answer Set Solvers, Intelligent Agents, Partial Assignment