scholarly journals Unsatisfiable Core Shrinking for Anytime Answer Set Optimization

2017 ◽  
Author(s):  
Mario Alviano ◽  
Carmine Dodaro
Keyword(s):  
Efficient Algorithms ◽  
Set Optimization ◽  
Core Analysis ◽  
Anytime Algorithm ◽  
Original Algorithm ◽  
Unsatisfiable Core ◽  
Stable Models ◽  
Answer Set

Efficient algorithms for the computation of optimum stable models are based on unsatisfiable core analysis. However, these algorithms essentially run to completion, providing few or even no suboptimal stable models. This drawback can be circumvented by shrinking unsatisfiable cores. Interestingly, the resulting anytime algorithm can solve more instances than the original algorithm.

scholarly journals Anytime answer set optimization via unsatisfiable core shrinking

2016 ◽  
Vol 16 (5-6) ◽  
pp. 533-551 ◽  
Author(s):  
MARIO ALVIANO ◽  
CARMINE DODARO
Keyword(s):  
Set Optimization ◽  
Core Analysis ◽  
Logic Programs ◽  
Anytime Algorithm ◽  
Shrinking Process ◽  
The One ◽  
Weak Constraints ◽  
Unsatisfiable Core ◽  
Stable Models ◽  
Answer Set

AbstractUnsatisfiable core analysis can boost the computation of optimum stable models for logic programs with weak constraints. However, current solvers employing unsatisfiable core analysis either run to completion, or provide no suboptimal stable models but the one resulting from the preliminary disjoint cores analysis. This drawback is circumvented here by introducing a progression based shrinking of the analyzed unsatisfiable cores. In fact, suboptimal stable models are possibly found while shrinking unsatisfiable cores, hence resulting into an anytime algorithm. Moreover, as confirmed empirically, unsatisfiable core analysis also benefits from the shrinking process in terms of solved instances.

Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

2020 ◽  
Vol 176 (3-4) ◽  
pp. 271-297
Author(s):  
Mario Alviano ◽  
Carmine Dodaro
Keyword(s):  
State Of The Art ◽  
Answer Set Programming ◽  
Efficient Algorithms ◽  
Satisfiability Problem ◽  
Core Analysis ◽  
Stable Model ◽  
Maximum Satisfiability ◽  
Model Search ◽  
Unsatisfiable Core ◽  
Stable Models

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

scholarly journals On the Semantics of Logic Programs with Preferences

2007 ◽  
Vol 30 ◽  
pp. 501-523 ◽  
Author(s):  
S. Greco ◽  
I. Trubitsyna ◽  
E. Zumpano
Keyword(s):  
Logic Programming ◽  
Complexity Analysis ◽  
Structural Information ◽  
Logic Program ◽  
Set Optimization ◽  
Logic Programs ◽  
Preference Relations ◽  
New Interpretation ◽  
Semantics Of Logic Programs ◽  
Stable Models

This work is a contribution to prioritized reasoning in logic programming in the presence of preference relations involving atoms. The technique, providing a new interpretation for prioritized logic programs, is inspired by the semantics of Prioritized Logic Programming and enriched with the use of structural information of preference of Answer Set Optimization Programming. Specifically, the analysis of the logic program is carried out together with the analysis of preferences in order to determine the choice order and the sets of comparable models. The new semantics is compared with other approaches known in the literature and complexity analysis is also performed, showing that, with respect to other similar approaches previously proposed, the complexity of computing preferred stable models does not increase.

scholarly journals Temporal logic programs with variables

2016 ◽  
Vol 17 (2) ◽  
pp. 226-243 ◽  
Author(s):  
FELICIDAD AGUADO ◽  
PEDRO CABALAR ◽  
GILBERTO PÉREZ ◽  
CONCEPCIÓN VIDAL ◽  
MARTÍN DIÉGUEZ
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Logic Program ◽  
Answer Set Programming ◽  
Logic Programs ◽  
First Order ◽  
Linear Time Temporal Logic ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractIn this note, we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic, an extension of Answer Set Programming for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of Temporal Equilibrium Logic that shares the syntax of first-order Linear-time Temporal Logic but has different semantics, selecting some Linear-time Temporal Logic models we call temporal stable models. Then, we consider a subclass of theories (called splittable temporal logic programs) that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of safe variables that suffices to show the property of domain independence – that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard Answer Set Programming grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

scholarly journals Module theorem for the general theory of stable models

2012 ◽  
Vol 12 (4-5) ◽  
pp. 719-735 ◽  
Author(s):  
JOSEPH BABB ◽  
JOOHYUNG LEE
Keyword(s):  
General Theory ◽  
General Class ◽  
Answer Set Programming ◽  
Splitting Theorem ◽  
Logic Programs ◽  
Input Output ◽  
Answer Sets ◽  
Output Interface ◽  
Stable Models ◽  
Answer Set

AbstractThe module theorem by Janhunen et al. demonstrates how to provide a modular structure in answer set programming, where each module has a well-defined input/output interface which can be used to establish the compositionality of answer sets. The theorem is useful in the analysis of answer set programs, and is a basis of incremental grounding and reactive answer set programming. We extend the module theorem to the general theory of stable models by Ferraris et al. The generalization applies to non-ground logic programs allowing useful constructs in answer set programming, such as choice rules, the count aggregate, and nested expressions. Our extension is based on relating the module theorem to the symmetric splitting theorem by Ferraris et al. Based on this result, we reformulate and extend the theory of incremental answer set computation to a more general class of programs.

scholarly journals DatalogMTL with Negation Under Stable Models Semantics

2021 ◽  
Author(s):  
Przemysław A. Wałęga ◽  
David J. Tena Cucala ◽  
Egor V. Kostylev ◽  
Bernardo Cuenca Grau
Keyword(s):  
Answer Set Programming ◽  
Data Complexity ◽  
Temporal Dimension ◽  
Temporal Direction ◽  
Stable Models ◽  
Answer Set

We introduce negation under stable models semantics in DatalogMTL—a temporal extension of Datalog with metric operators. As a result, we obtain a rule language which combines the power of answer set programming with the temporal dimension provided by metric operators. We show that, in this setting, reasoning becomes undecidable over the rationals and decidable in EXPSPACE in data complexity over the integers. We also show that, if we restrict our attention to forward-propagating programs (where rules propagate information in a single temporal direction), reasoning over integers becomes PSPACE-complete in data complexity and hence no harder than over positive programs; however, reasoning over the rationals in this fragment remains undecidable.

scholarly journals Strong Equivalence of Qualitative Optimization Problems

2013 ◽  
Vol 47 ◽  
pp. 351-391
Author(s):  
W. Faber ◽  
M. Truszczyński ◽  
S. Woltran
Keyword(s):  
Equilibrium Model ◽  
Propositional Logic ◽  
Optimization Problems ◽  
Modular Representation ◽  
Set Optimization ◽  
Propositional Theory ◽  
Reasoning Tasks ◽  
Answer Set Semantics ◽  
The Way ◽  
Answer Set

We introduce the framework of qualitative optimization problems (or, simply, optimization problems) to represent preference theories. The formalism uses separate modules to describe the space of outcomes to be compared (the generator) and the preferences on outcomes (the selector). We consider two types of optimization problems. They differ in the way the generator, which we model by a propositional theory, is interpreted: by the standard propositional logic semantics, and by the equilibrium-model (answer-set) semantics. Under the latter interpretation of generators, optimization problems directly generalize answer-set optimization programs proposed previously. We study strong equivalence of optimization problems, which guarantees their interchangeability within any larger context. We characterize several versions of strong equivalence obtained by restricting the class of optimization problems that can be used as extensions and establish the complexity of associated reasoning tasks. Understanding strong equivalence is essential for modular representation of optimization problems and rewriting techniques to simplify them without changing their inherent properties.

Sign in / Sign up

Export Citation Format

Share Document