On the tractability of minimal model computation for some CNF theories

DOI10.1016/J.ARTINT.2014.02.003zbMATH Open1334.68205arXiv1310.8120OpenAlexW2021305476MaRDI QIDQ490649FDOQ490649

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

Publication date: 27 August 2015

Published in: Artificial Intelligence (Search for Journal in Brave)

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.

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

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

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)

Cites Work

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

Cited In (8)

• On the computability-theoretic complexity of trivial, strongly minimal models
• Title not available (Why is that?)
• Paracoherent answer set computation
• Title not available (Why is that?)
• Computing minimal models, stable models and answer sets
• Better Paracoherent Answer Sets with Less Resources
• Title not available (Why is that?)
• Graph-based construction of minimal models

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)