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.

Optimum stable model search: algorithms and implementation

2015 ◽  
Vol 30 (4) ◽  
pp. 863-897 ◽  
Author(s):  
Mario Alviano ◽  
Carmine Dodaro ◽  
Joao Marques-Silva ◽  
Francesco Ricca
Keyword(s):  
Optimization Problems ◽  
Nonmonotonic Reasoning ◽  
Answer Set Programming ◽  
Stable Model ◽  
Combinatorial Search ◽  
Maximum Satisfiability ◽  
Model Search ◽  
Pros And Cons ◽  
Satisfiability Solving ◽  
Weak Constraints

Abstract Answer Set Programming (ASP) is a well-known declarative problem solving paradigm developed in the field of nonmonotonic reasoning and logic programming. The usual target of ASP is the solution of combinatorial search problems, nonetheless the language of ASP was extended with weak constraints for concise modelling of optimization problems. In the case of ASP programs with weak constraints, the main computational task of an ASP solver is optimum stable model search . In this article, we present and compare several algorithms for optimum stable model search. We consider solutions traditionally adopted by ASP solvers, and we introduce new solving strategies obtained by porting to the ASP setting some algorithms that were introduced for Maximum Satisfiability solving. The article also reports on the implementation of these algorithms in the ASP solver wasp . An empirical analysis highlights pros and cons of different strategies for computing optimum stable models.

scholarly journals Cautious reasoning in ASP via minimal models and unsatisfiable cores

2018 ◽  
Vol 18 (3-4) ◽  
pp. 319-336 ◽  
Author(s):  
MARIO ALVIANO ◽  
CARMINE DODARO ◽  
MATTI JÄRVISALO ◽  
MARCO MARATEA ◽  
ALESSANDRO PREVITI
Keyword(s):  
Knowledge Representation ◽  
State Of The Art ◽  
Answer Set Programming ◽  
Query Answering ◽  
Stable Model ◽  
Minimal Models ◽  
Input Program ◽  
New Algorithms ◽  
Better Than ◽  
Stable Models

AbstractAnswer Set Programming (ASP) is a logic-based knowledge representation framework, supporting—among other reasoning modes—the central task of query answering. In the propositional case, query answering amounts to computing cautious consequences of the input program among the atoms in a given set of candidates, where a cautious consequence is an atom belonging to all stable models. Currently, the most efficient algorithms either iteratively verify the existence of a stable model of the input program extended with the complement of one candidate, where the candidate is heuristically selected, or introduce a clause enforcing the falsity of at least one candidate, so that the solver is free to choose which candidate to falsify at any time during the computation of a stable model. This paper introduces new algorithms for the computation of cautious consequences, with the aim of driving the solver to search for stable models discarding more candidates. Specifically, one of such algorithms enforces minimality on the set of true candidates, where different notions of minimality can be used, and another takes advantage of unsatisfiable cores computation. The algorithms are implemented inwasp, and experiments on benchmarks from the latest ASP competitions show that the new algorithms perform better than the state of the art.

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.

scholarly journals Symmetry breaking in a new stable model search method

10.29007/1l5r ◽  
2018 ◽  
Author(s):  
Tarek Khaled ◽  
Belaid Benhamou
Keyword(s):  
Knowledge Representation ◽  
Symmetry Breaking ◽  
Constraint Programming ◽  
Answer Set Programming ◽  
Search Tree ◽  
Search Method ◽  
Combinatorial Problems ◽  
Knowledge Representation And Reasoning ◽  
Stable Model ◽  
Model Search

In this work, we investigate the inclusion of symmetry breaking in the answer set programming (ASP) framework. The notion of symmetry is widely studied in various domains. Particularly, in the field of constraint programming, where symmetry breaking made a significant improvement in the performances of many constraint solvers. Usually, combinatorial problems contain a lot of symmetries that could render their resolution difficult for the solvers that do not consider them. Indeed, these symmetries guide the solvers in the useless exploration of symmetric and redundant branches of the search tree. The ASP framework is well-known in knowledge representation and reasoning. How- ever, only few works on symmetry in ASP exist. We propose in this paper a new ASP solver based on a novel semantics that we enhance by symmetry breaking. This method with symmetry elimination is implemented and used for the resolution of a large variety of combinatorial problems. The obtained results are very promising and showcase an advantage when using our method in comparison to other known ASP methods.

scholarly journals On equivalence of infinitary formulas under the stable model semantics

2014 ◽  
Vol 15 (1) ◽  
pp. 18-34 ◽  
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ ◽  
MIROSLAW TRUSZCZYNSKI
Keyword(s):  
Intuitionistic Logic ◽  
Answer Set Programming ◽  
Stable Model ◽  
Stable Models ◽  
Answer Set

AbstractPropositional formulas that are equivalent in intuitionistic logic, or in its extension known as the logic of here-and-there, have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show how to apply this generalization to proving properties of aggregates in answer set programming.

scholarly journals Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem

2009 ◽  
Vol 36 ◽  
pp. 229-266 ◽  
Author(s):  
H.L. Chieu ◽  
W.S. Lee
Keyword(s):  
Phase Transition ◽  
State Of The Art ◽  
Satisfiability Problem ◽  
Maximum Satisfiability ◽  
Sat Problem ◽  
Sat Solvers ◽  
Minimal Weight ◽  
Survey Propagation ◽  
Max Sat

The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.

scholarly journals Relating Two Dialects of Answer Set Programming

2019 ◽  
Vol 19 (5-6) ◽  
pp. 1006-1020 ◽  
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ
Keyword(s):  
Working Group ◽  
Answer Set Programming ◽  
Stable Model ◽  
Input Language ◽  
Core Language ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractThe input language of the answer set solver clingo is based on the definition of a stable model proposed by Paolo Ferraris. The semantics of the ASP-Core language, developed by the ASP Standardization Working Group, uses the approach to stable models due to Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. The two languages are based on different versions of the stable model semantics, and the ASP-Core document requires, “for the sake of an uncontroversial semantics,” that programs avoid the use of recursion through aggregates. In this paper we prove that the absence of recursion through aggregates does indeed guarantee the equivalence between the two versions of the stable model semantics, and show how that requirement can be relaxed without violating the equivalence property.

Algorithms for the maximum satisfiability problem

Computing ◽  
1990 ◽  
Vol 44 (4) ◽  
pp. 279-303 ◽  
Author(s):  
Pierre Hansen ◽  
Brigitte Jaumard
Keyword(s):  
Satisfiability Problem ◽  
Maximum Satisfiability

The interpretation of unsolvable λ-terms in models of untyped λ-calculus

1998 ◽  
Vol 63 (4) ◽  
pp. 1529-1548 ◽  
Author(s):  
Rainer Kerth
Keyword(s):  
Graph Model ◽  
Stable Model ◽  
Graph Models ◽  
Stable Models

AbstractOur goal in this paper is to analyze the interpretation of arbitrary unsolvable λ-terms in a given model of λ-calculus. We focus on graph models and (a special type of) stable models. We introduce the syntactical notion of a decoration and the semantical notion of a critical sequence. We conjecture that any unsolvable term β-reduces to a term admitting a decoration. The main result of this paper concerns the interconnection between those two notions: given a graph model or stable model , we show that any unsolvable term admitting a decoration and having a non-empty interpretation in generates a critical sequence in the model.In the last section, we examine three classical graph models, namely the model of Plotkin and Scott, Engeler's model and Park's model . We show that and do not contain critical sequences whereas does.

Sign in / Sign up

Export Citation Format

Share Document