Model enumeration in propositional circumscription via unsatisfiable core analysis
From MaRDI portal
Publication:4592705
Abstract: Many practical problems are characterized by a preference relation over admissible solutions, where preferred solutions are minimal in some sense. For example, a preferred diagnosis usually comprises a minimal set of reasons that is sufficient to cause the observed anomaly. Alternatively, a minimal correction subset comprises a minimal set of reasons whose deletion is sufficient to eliminate the observed anomaly. Circumscription formalizes such preference relations by associating propositional theories with minimal models. The resulting enumeration problem is addressed here by means of a new algorithm taking advantage of unsatisfiable core analysis. Empirical evidence of the efficiency of the algorithm is given by comparing the performance of the resulting solver, CIRCUMSCRIPTINO, with HCLASP, CAMUS MCS, LBX and MCSLS on the enumeration of minimal models for problems originating from practical applications. This paper is under consideration for acceptance in TPLP.
Recommendations
Cites work
- Advances in WASP
- Algorithms for computing minimal unsatisfiable subsets of constraints
- Answer set enumeration via assumption literals
- Answer set programming based on propositional satisfiability
- Anytime answer set optimization via unsatisfiable core shrinking
- ASSAT: computing answer sets of a logic program by SAT solvers
- Circumscription - a form of non-monotonic reasoning
- Complexity and compilation of GZ-aggregates in answer set programming
- Computing Diverse Optimal Stable Models
- Conflict-Driven Answer Set Enumeration
- Conflict-driven answer set solving: from theory to practice
- Cores in core based MaxSat algorithms: an analysis
- Evaluating Answer Set Programming with Non-Convex Recursive Aggregates
- Implementing preferences with asprin
- Iterative and core-guided maxsat solving: a survey and assessment
- Logic Programming
- Logic programming, knowledge representation, and nonmonotonic reasoning. Essays dedicated to Michael Gelfond on the occasion of his 65th birthday
- Loop formulas for circumscription
- MCS Extraction with Sublinear Oracle Queries
- Minimal intervention strategies in logical signaling networks with ASP
- On computing preferred MUSes and MCSes
- On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers
- On the satisfiability of circumscription
- optsat: A Tool for Solving SAT Related Optimization Problems
- Parallel model-based diagnosis on multi-core computers
- Progress in clasp series 3
- Rewriting recursive aggregates in answer set programming: back to monotonicity
- Solving set optimization problems by cardinality optimization with an application to argumentation
- The ASP system DLV2
- The Complexity Boundary of Answer Set Programming with Generalized Atoms under the FLP Semantics
- The DLV system for knowledge representation and reasoning
- Unsatisfiability-based optimization in clasp
Cited in
(8)- Design and results of the second international competition on computational models of argumentation
- Strong inconsistency
- Cautious reasoning in ASP via minimal models and unsatisfiable cores
- ASP and subset minimality: enumeration, cautious reasoning and MUSes
- Computing MUS-based inconsistency measures
- Strong backdoors for default logic
- Strong backdoors for default logic
- A MaxSAT-based framework for computing circumscription
Describes a project that uses
Uses Software
This page was built for publication: Model enumeration in propositional circumscription via unsatisfiable core analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592705)
