Disjunctive answer set solvers via templates

DOI10.1017/S1471068415000411MaRDI QIDQ4593037zbMATH OpenOpenAlexFDO

Authors Rémi Brochenin, Marco Maratea, Yuliya Lierler

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

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

zbMATH Keywords

abstract solversanswer set programming

Mathematics Subject Classification ID

Logic programming (68N17) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is $Sigm{a}_2^P$-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely DLV, GnT, Cmodels, CLASP and WASP. In this paper we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers DLV, GnT and Cmodels. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers.

Recommendations

• scientific article; zbMATH DE number 6747884
• scientific article; zbMATH DE number 5079838
• scientific article; zbMATH DE number 1292288
• scientific article; zbMATH DE number 1931680
• Disjunctive logic programs, answer sets, and the cut rule
• Abstract Answer Set Solvers
• Solving disjunctive fuzzy answer set programs
• Declarative Problem Solving Using Answer Set Semantics
• scientific article; zbMATH DE number 1213132

Cites work

• A machine program for theorem-proving
• Abstract Answer Set Solvers
• Abstract answer set solvers with backjumping and learning
• Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation
• Enhancing disjunctive logic programming systems by SAT checkers
• Enhancing DLV instantiator by backjumping techniques
• Extending and implementing the stable model semantics
• scientific article; zbMATH DE number 25190 (Why is no real title available?)
• scientific article; zbMATH DE number 1368933 (Why is no real title available?)
• scientific article; zbMATH DE number 1884395 (Why is no real title available?)
• scientific article; zbMATH DE number 6747884 (Why is no real title available?)
• Inferring phylogenetic trees using answer set programming
• Knowledge Representation, Reasoning and Declarative Problem Solving
• Logic Programming
• Logic programming and nonmonotonic reasoning. 12th international conference, LPNMR 2013, Corunna, Spain, September 15--19, 2013. Proceedings
• Logic programming and nonmonotonic reasoning. 8th international conference, LPNMR 2005, Diamante, Italy, September 5--8, 2005. Proceedings.
• Logic programs with stable model semantics as a constraint programming paradigm
• On the relation among answer set solvers
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Tableau Calculi for Answer Set Programming
• Tableau calculi for logic programs under answer set semantics
• Team-building with answer set programming in the Gioia-Tauro seaport
• The DLV system for knowledge representation and reasoning
• Transition systems for model generators -- a unifying approach
• Unfolding partiality and disjunctions in stable model semantics

Cited in

(6)

• Transition systems for model generators -- a unifying approach
• scientific article; zbMATH DE number 5079838 (Why is no real title available?)
• Towards automated integration of guess and check programs in answer set programming: a meta-interpreter and applications
• scientific article; zbMATH DE number 1931680 (Why is no real title available?)
• scientific article; zbMATH DE number 6747884 (Why is no real title available?)
• Abstract Answer Set Solvers

Describes a project that uses

Uses Software

• WASP
• Cmodels
• Datalog

This page was built for publication: Disjunctive answer set solvers via templates

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