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.

Reduct-based Stability Check Using Literal Assumptions

Alviano M.;Dodaro C.;Ricca F.
2015-01-01

Abstract

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.
2015
Answer Set Programming
Computational Tasks
Model Checker
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/306320
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact