Reduct-based Stability Check Using Literal Assumptions

For disjunctive logic programs, checking the stability of a model is a co-NP-complete task in general. The first implementations of this task were found on checking the unsatisfiability of a propositional formula whose construction is based on the reduct of the input program with respect to the model to be checked. Even if such a formula can be built in polynomial time, in practice its creation is often more expensive than the unsatisfiability check. A different strategy was implemented in clasp, where an alternative characterization of stable models based on unfounded sets is used to obtain a propositional formula that can be reused for all stability checks in conjunction with literal assumptions. However, the question whether the early approach based on program reducts can be rethought in terms of literal assumptions remained unanswered so far. A positive answer is provided here by introducing a reduct-based strategy for stability check using literal assumptions, which is also implemented in the ASP solver wasp2. The viability of the new technique is confirmed by a preliminary experimental analysis reported in the paper.