On the tractability of minimal model computation for some CNF theories

DOI10.1016/J.ARTINT.2014.02.003MaRDI QIDQ490649zbMATH OpenOpenAlexFDO

Authors Fabrizio Angiulli, Rachel Ben-Eliyahu-Zohary, Fabio Fassetti, Luigi Palopoli

Publication date 27 August 2015

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1310.8120

zbMATH Keywords

computational complexityminimal modelCNF theorieshead-cycle-free CNF theorieshead-elementary-set-free CNF theories

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in artificial intelligence (68T27)

Abstract: Designing algorithms capable of efficiently constructing minimal models of CNFs is an important task in AI. This paper provides new results along this research line and presents new algorithms for performing minimal model finding and checking over positive propositional CNFs and model minimization over propositional CNFs. An algorithmic schema, called the Generalized Elimination Algorithm (GEA) is presented, that computes a minimal model of any positive CNF. The schema generalizes the Elimination Algorithm (EA) [BP97], which computes a minimal model of positive head-cycle-free (HCF) CNF theories. While the EA always runs in polynomial time in the size of the input HCF CNF, the complexity of the GEA depends on the complexity of the specific eliminating operator invoked therein, which may in general turn out to be exponential. Therefore, a specific eliminating operator is defined by which the GEA computes, in polynomial time, a minimal model for a class of CNF that strictly includes head-elementary-set-free (HEF) CNF theories [GLL06], which form, in their turn, a strict superset of HCF theories. Furthermore, in order to deal with the high complexity associated with recognizing HEF theories, an "incomplete" variant of the GEA (called IGEA) is proposed: the resulting schema, once instantiated with an appropriate elimination operator, always constructs a model of the input CNF, which is guaranteed to be minimal if the input theory is HEF. In the light of the above results, the main contribution of this work is the enlargement of the tractability frontier for the minimal model finding and checking and the model minimization problems.

Recommendations

• On computing minimal models
• Reasoning with minimal models: efficient algorithms and applications
• Computing minimal models, stable models and answer sets
• Logic Programming
• Modular construction of minimal models

Cites work

• scientific article; zbMATH DE number 3755910 (Why is no real title available?)
• scientific article; zbMATH DE number 25190 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 2038901 (Why is no real title available?)
• scientific article; zbMATH DE number 5215800 (Why is no real title available?)
• scientific article; zbMATH DE number 956863 (Why is no real title available?)
• A logic for default reasoning
• An incremental algorithm for generating all minimal models
• Characterizing diagnoses and systems
• Circumscription - a form of non-monotonic reasoning
• Computing minimal models, stable models and answer sets
• Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation
• Handbook of knowledge representation.
• Head-Elementary-Set-Free Logic Programs
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• On computing minimal models
• On the complexity of identifying head-elementary-set-free programs
• Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
• Propositional semantics for disjunctive logic programs
• Reasoning with minimal models: efficient algorithms and applications
• Some computational aspects of circumscription
• Stochastic local search. Foundations and applications.
• The complexity of minimal satisfiability problems
• The complexity of model checking for circumscriptive formulae

Cited in

(9)

• Graph-based construction of minimal models
• Better paracoherent answer sets with less resources
• Logic Programming
• scientific article; zbMATH DE number 2026795 (Why is no real title available?)
• scientific article; zbMATH DE number 5215800 (Why is no real title available?)
• Paracoherent answer set computation
• scientific article; zbMATH DE number 1884382 (Why is no real title available?)
• Computing minimal models, stable models and answer sets
• On the computability-theoretic complexity of trivial, strongly minimal models

Describes a project that uses

Uses Software

• Walksat

This page was built for publication: On the tractability of minimal model computation for some CNF theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q490649)