TY - GEN

T1 - Fast SAT-based answer set solver

AU - Lin, Zhijun

AU - Zhang, Yuanlin

AU - Hemandez, Hector

PY - 2006

Y1 - 2006

N2 - 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 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. In the few cases when it is not the winner, it is close to the top performer, which shows its robustness.

AB - 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 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. In the few cases when it is not the winner, it is close to the top performer, which shows its robustness.

UR - http://www.scopus.com/inward/record.url?scp=33750740382&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:33750740382

SN - 1577352815

SN - 9781577352815

T3 - Proceedings of the National Conference on Artificial Intelligence

SP - 92

EP - 97

BT - Proceedings of the 21st National Conference on Artificial Intelligence and the 18th Innovative Applications of Artificial Intelligence Conference, AAAI-06/IAAI-06

Y2 - 16 July 2006 through 20 July 2006

ER -