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