Abstract Solvers for Computing Cautious Consequences of ASP programs
Abstract solvers are a method to formally analyze algorithms that have been profitably used for describing, comparing and composing solving techniques in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP. In this paper, we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers for cautious reasoning in ASP with new techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. By doing so, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. We implement some of the new solutions in the ASP solver WASP and show that their performance are comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions. Under consideration for acceptance in TPLP.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Anytime Computation of Cautious Consequences in Answer Set Programming
Query answering in Answer Set Programming (ASP) is usually solved by computing (a subset of) the cautious consequences of a logic program. This task is computationally very hard, and there are programs for which computin…
eclingo: A solver for Epistemic Logic Programs
We describe eclingo, a solver for epistemic logic programs under Gelfond 1991 semantics built upon the Answer Set Programming system clingo. The input language of eclingo uses the syntax extension capabilities of clingo …
Solving Epistemic Logic Programs using Generate-and-Test with Propagation
This paper introduces a general framework for generate-and-test-based solvers for epistemic logic programs that can be instantiated with different generator and tester programs, and we prove sufficient conditions on thos…
Abstract Modular Systems and Solvers
Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience and computational benefits. We introduce concepts of abstract modules and abstract modular …
System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of …