Stable Model Checking (MC) in Answer Set Programming systems is, in general, a co-NP task for disjunctive programs. Thus, implementing an efficient strategy is very important for the performance of ASP systems. In DLV, MC is carried out by exploiting the SAT solver SATZ, and the result of this operation also returns (in case the check fails) an "unfounded set", as by-product, which is also used for pruning the search space during answer set computation. In this paper we report on the integration of a "modern" SAT solver, MINISAT, in DLV. The integration poses not only technological issues, but also challenges w.r.t. the "quality" of the returned unfounded set and w.r.t. the interplay with the existing DLV techniques.
展开▼
