Integrating Answer Set Programming and Satisfiability Modulo Theories

Declarative Programming ◽

Scheduling Problems ◽

New Horizons ◽

Research Areas ◽

Constraint Processing ◽

Abstract Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. CASP demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt2smt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Traveling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP.

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence ◽

A Formal Approach for Cautious Reasoning in Answer Set Programming (Extended Abstract)

10.24963/ijcai.2020/652 ◽

2020 ◽

Author(s):

Giovanni Amendola ◽

Carmine Dodaro ◽

Marco Maratea

Keyword(s):

Answer Set Programming ◽

Propositional Satisfiability ◽

Formal Approach ◽

Boolean Formulas ◽

Reasoning Tasks ◽

The issue of describing in a formal way solving algorithms in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP, has been relatively recently solved employing abstract solvers. In this paper we deal with cautious reasoning tasks in ASP, and design, implement and test novel abstract solutions, borrowed from backbone computation in SAT. By employing abstract solvers, 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. Some of the new solutions have been implemented in the ASP solver WASP, and tested.

Fuzzy answer set computation via satisfiability modulo theories

10.1017/s1471068415000241 ◽

2015 ◽

Vol 15 (4-5) ◽

pp. 588-603 ◽

Cited By ~ 4

Author(s):

MARIO ALVIANO ◽

RAFAEL PEÑALOZA

Keyword(s):

Fuzzy Logic ◽

Structural Properties ◽

Answer Set Programming ◽

Prototype System ◽

Imprecise Information ◽

Fuzzy Connectives ◽

AbstractFuzzy answer set programming (FASP) combines two declarative frameworks, answer set programming and fuzzy logic, in order to model reasoning by default over imprecise information. Several connectives are available to combine different expressions; in particular the Gödel and Łukasiewicz fuzzy connectives are usually considered, due to their properties. Although the Gödel conjunction can be easily eliminated from rule heads, we show through complexity arguments that such a simplification is infeasible in general for all other connectives. The paper analyzes a translation of FASP programs into satisfiability modulo theories (SMT), which in general produces quantified formulas because of the minimality of the semantics. Structural properties of many FASP programs allow to eliminate the quantification, or to sensibly reduce the number of quantified variables. Indeed, integrality constraints can replace recursive rules commonly used to force Boolean interpretations, and completion subformulas can guarantee minimality for acyclic programs with atomic heads. Moreover, head cycle free rules can be replaced by shifted subprograms, whose structure depends on the eliminated head connective, so that ordered completion may replace the minimality check if also Łukasiewicz disjunction in rule bodies is acyclic. The paper also presents and evaluates a prototype system implementing these translations.

Abstract Solvers for Computing Cautious Consequences of ASP programs

10.1017/s1471068419000164 ◽

2019 ◽

Vol 19 (5-6) ◽

pp. 740-756

Author(s):

GIOVANNI AMENDOLA ◽

CARMINE DODARO ◽

MARCO MARATEA

Keyword(s):

State Of The Art ◽

Answer Set Programming ◽

Benchmark Problems ◽

Propositional Satisfiability ◽

New Techniques ◽

The Past ◽

Boolean Formulas ◽

Reasoning Tasks ◽

AbstractAbstract 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.

On relation between constraint answer set programming and satisfiability modulo theories

10.1017/s1471068417000114 ◽

2017 ◽

Vol 17 (4) ◽

pp. 559-590

Author(s):

YULIYA LIERLER ◽

BENJAMIN SUSMAN

Keyword(s):

Answer Set Programming ◽

Research Direction ◽

Linear Constraints ◽

Research Areas ◽

Formal Relation ◽

Answer Sets ◽

Theoretical Foundations ◽

Cross Fertilization ◽

AbstractConstraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will boost the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction, we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs.

Non-monotonic spatial reasoning with answer set programming modulo theories

10.1017/s1471068416000193 ◽

2016 ◽

Vol 17 (2) ◽

pp. 205-225 ◽

Cited By ~ 2

Author(s):

PRZEMYSŁAW ANDRZEJ WAŁĘGA ◽

CARL SCHULTZ ◽

MEHUL BHATT

Keyword(s):

Spatial Reasoning ◽

Answer Set Programming ◽

Spatial Relations ◽

Cognitive Robotics ◽

Spatial Effects ◽

Novel Approach ◽

Spatial Systems ◽

Wide Range ◽

AbstractThe systematic modelling ofdynamic spatial systemsis a key requirement in a wide range of application areas such as commonsense cognitive robotics, computer-aided architecture design, and dynamic geographic information systems. We present Answer Set Programming Modulo Theories (ASPMT)(QS), a novel approach and fully implemented prototype for non-monotonic spatial reasoning — a crucial requirement within dynamic spatial systems — based on ASPMT. ASPMT(QS) consists of a (qualitative) spatial representation module (QS) and a method for turning tight ASPMT instances into Satisfiability Modulo Theories (SMT) instances in order to compute stable models by means of SMT solvers. We formalise and implement concepts of default spatial reasoning and spatial frame axioms. Spatial reasoning is performed by encoding spatial relations as systems of polynomial constraints, and solving via SMT with the theory of real non-linear arithmetic. We empirically evaluate ASPMT(QS) in comparison with other contemporary spatial reasoning systems both within and outside the context of logic programming. ASPMT(QS) is currently the only existing system that is capable of reasoning about indirect spatial effects (i.e., addressing the ramification problem), and integrating geometric and QS information within a non-monotonic spatial reasoning context.