Physical Sciences and Mathematics Commons^™

Performance Tuning In Answer Set Programming, Matt Buddenhagen, Yuliya Lierler

Yuliya Lierler

Constraint Answer Set Programming Versus Satisfiability Modulo Theories Or Constraints Versus Theories, Yuliya Lierler, Benjamin Susman

Yuliya Lierler

An Abstract View On Modularity In Knowledge Representation, Yuliya Lierler, Miroslaw Truszczyński

Yuliya Lierler

Modularity is an essential aspect of knowledge representation and reasoning theory and practice. It has received substantial attention. We introduce model-based modular systems, an abstract framework for modular knowledge representation formalisms, similar in scope to multi-context systems but employing a simpler information-flow mechanism. We establish the precise relationship between the two frameworks, showing that they can simulate each other. We demonstrate that recently introduced modular knowledge representation formalisms integrating logic programming with satisfiability and, more generally, with constraint satisfaction can be cast as modular systems in our sense. These results show that our formalism offers a simple unifying framework for …

Abstract Disjunctive Answer Set Solvers, Remi Brochenin, Yuliya Lierler, Marco Maratea

Yuliya Lierler

A fundamental task in answer set programming is to compute answer sets of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has an answer set isΣP2 -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 and CLASP. 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. In particular, we present transition systems for CMODELS (without backjumping …

Abstract Modular Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński

Yuliya Lierler

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 systems to study general principles behind the design and analysis of modelfinding programs, or solvers, for integrated heterogeneous multi-logic systems. We show how abstract modules and abstract modular systems give rise to transition systems, which are a natural and convenient representation of solvers pioneered by the SAT community. We illustrate our approach by showing how it applies to answer set programming and propositional logic, and to multi-logic systems based on these two formalisms.

Asp-Based Problem Solving With Cutting-Edge Tools, Marcello Balduccini, Yuliya Lierler

Yuliya Lierler

In the development of practical applications of answer set programming (ASP), encodings that use well-established solvers such as CLASP and DLV are sometimes affected by scalability issues. In those situations, one can resort to more sophisticated ASP tools exploiting, for instance, incremental and constraint ASP. However, today there is no specific methodology for the selection or use of such tools. In this paper we describe how we used such cutting-edge ASP tools on challenging problems from the Third Answer Set Programming Competition, and outline the methodology we followed. We view this paper as a first step in the development of …

A Transition System For Ac Language Algorithms, Yuliya Lierler, Yaunlin Zhang

Yuliya Lierler

Recently a logic programming language AC was proposed by Mellarkod et al. (2008) to integrate answer set programming (ASP) and constraint logic programming. In a similar vein, Gebser et al. (2009) proposed a CLINGCON language integrating ASP and finite domain constraints. A distinguishing feature of these languages is their capacity to allow new efficient inference algorithms that combine traditional ASP procedures and other efficient methods in constraint programming. In this paper we show that a transition system introduced by Nieuwenhuis et al. (2006) can be extended to model the “hybrid” ACSOLVER algorithm, by Mellarkod et al., designed for processing a …

Hybrid Automated Reasoning Tools: From Black-Box To Clear-Box Integration, Marcello Balduccini, Yuliya Lierler

Yuliya Lierler

Recently, researchers in answer set programming and constraint programming spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming (CASP). CASP languages and systems proved to be largely successful at providing efficient solutions to problems involving hybrid reasoning tasks, such as scheduling problems with elements of planning. Yet, the development of CASP systems is difficult, requiring non-trivial expertise in multiple areas. This suggests a need for a study identifying general development principles of hybrid systems. Once these principles …

Representing Synonymity In Causal Logic And In Logic Programming, Joohyung Lee, Yuliya Lierler, Vladimir Lifschitz, Fangkai Yang

Yuliya Lierler

We investigate the relationship between rules representing synonymity in nonmonotonic causal logic and in answer set programming. This question is of interest in connection with current work on modular languages for describing actions.

A Sat-Based Polynomial Space Algorithm For Answer Set Programming, Enrico Giunchiglia, Marco Maratea, Yuliya Lierler

Yuliya Lierler

The relation between answer set programming (ASP) and propositional satisfiability (SAT) is at the center of many research papers, partly because of the tremendous performance boost of SAT solvers during last years. Various translations from ASP to SAT are known but the resulting SAT formula either includes many new variables or may have an unpractical size. There are also well known results showing a one-to-one correspondence between the answer sets of a logic program and the models of its completion. Unfortunately, these results only work for specific classes of problems. In this paper we present a SAT-Based decision procedure for …

Fages' Theorem And Answer Set Programming, Yuliya Lierler, Esta Erdem, Vladimir Lifschitz

Yuliya Lierler

We generalize a theorem by François Fages that describes the relationship between the completion semantics and the answer set semantics for logic programs with negotiation as failure. The study of this relationship is important in connection with the emergence of answer set programming. Whenever the two semantics are equivalent, answer sets can be computed by a satisfiability solver, and the use of answer set solvers such as SMODELS and DLV is unnecessary. A logic programming representation of the blocks world due to Ilkka Niemelä is discussed as an example.

Integration Schemas For Constraint Answer Set Programming: A Case Study, Marcello Balduccini, Yuliya Lierler

Yuliya Lierler

Recently, researchers in answer set programming and constraint programming spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming (CASP). CASP languages and systems proved to be largely successful at providing efficient solutions to problems involving hybrid reasoning tasks, such as scheduling problems with elements of planning. Yet, the development of CASP systems is difficult, requiring non-trivial expertise in multiple areas. This suggests a need for a study identifying general development principles of hybrid systems. Once these principles …

Answer Set Programming Based On Propositional Satisfiability, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea

Yuliya Lierler

Answer set programming (ASP) emerged in the late 1990s as a new logic programming paradigm that has been successfully applied in various application domains. Also motivated by the availability of efficient solvers for propositional satisfiability (SAT), various reductions from logic programs to SAT were introduced. All these reductions, however, are limited to a subclass of logic programs or introduce new variables or may produce exponentially bigger propositional formulas. In this paper, we present a SAT-based procedure, called ASPSAT, that (1) deals with any (nondisjunctive) logic program, (2) works on a propositional formula without additional variables (except for those possibly introduced …

Abstract Answer Set Solvers, Yuliya Lierler

Yuliya Lierler

Nieuwenhuis, Oliveras, and Tinelli showed how to describe enhancements of the Davis-Putnam-Logemann-Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for three algorithms that generate answer sets for logic programs: SMODELS, ASP-SAT with Backtracking, and a newly designed and implemented algorithm SUP. This approach to describing answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.

Cmodels For Tight Disjunctive Logic Programs, Yuliya Lierler

Yuliya Lierler

Disjunctive logic programming under the stable model semantics [GL91] is a new answer set programming (ASP) methodology for solving combinatorial search problems. It is a form of declarative programming related to logic programming languages, such as Prolog, where the solutions to a problem are represented by answer sets, and not by answer substitutions produced in response to a query as in convential logic programming. Instead of Prolog systems, this programming method uses answer set solvers, such as smodels1, smodelscc2, cmodels3, dlv4, and gnt1. These systems made it possible for ASP to be successfully applied in such areas as planning, bounded …

Relating Constraint Answer Set Programming Languages And Algorithms, Yuliya Lierler

Yuliya Lierler

Recently a logic programming language AC was proposed by Mellarkod et al. (2008) to integrate answer set programming and constraint logic programming. Soon after that, a CLINGCON language integrating answer set programming and finite domain constraints, as well as an EZCSP language integrating answer set programming and constraint logic programming were introduced. The development of these languages and systems constitutes the appearance of a new AI subarea called constraint answer set programming. All these languages have something in common. In particular, they aim at developing new efficient inference algorithms that combine traditional answer set programming procedures and other methods in …

Practical And Methodological Aspects Of The Use Of Cutting-Edge Asp Tools, Marcello Balduccini, Yuliya Lierler

Yuliya Lierler

In the development of practical applications of answer set programming (ASP), encodings that use well-established solvers such as CLASP and DLV are sometimes affected by scalability issues. In those situations, one can resort to more sophisticated ASP tools exploiting, for instance, incremental and constraint ASP. However, today there is no specific methodology for the selection or use of such tools. In this paper we describe how we used such cutting-edge ASP tools on challenging problems from the Third Answer Set Programming Competition. We view this paper as a first step in the development of a general methodology for the use …

On The Relation Of Constraint Answer Set Programming Languages And Algorithms, Yuliya Lierler

Yuliya Lierler

Recently a logic programming language AC was proposed by Mellarkod et al. (2008) to integrate answer set programming (ASP) and constraint logic programming. Similarly, Gebser et al. (2009) proposed a CLINGCON language integrating ASP and finite domain constraints. These languages allow new efficient inference algorithms that combine traditional ASP procedures and other methods in constraint programming. In this paper we show that a transition system introduced by Nieuwenhuis et al. (2006) to model SAT solvers can be extended to model the “hybrid” ACSOLVER algorithm by Mellarkod et al. developed for simple AC programs and the CLINGCON algorithm by Gebser et …

Constraint Answer Set Programming, Yuliya Lierler

Yuliya Lierler

Constraint answer set programming (CASP) is a novel, promising direction of research whose roots go back to propositional satisfiability (SAT). SAT solvers are efficient tools for solving boolean constraint satisfaction problems that arise in different areas of computer science, including software and hardware verification. Some constraints are more naturally expressed by non-boolean constructs. Satisfiability modulo theories (SMT) extends boolean satisfiability by the integration of non-boolean symbols defined by a background theory in another formalism, such as a constraint processing language. Answer set programming (ASP) extends computational methods of SAT in yet another way, inspired by ideas from knowledge representation, logic …

When Are Behaviour Networks Well-Behaved?, Bernhard Nebel, Yuliya Lierler

Yuliya Lierler

Agents operating in the real world have to deal with a constantly changing and only partially predictable environment and are nevertheless expected to choose reasonable actions quickly. This problem is addressed by a number of action-selection mechanisms. Behaviour networks as proposed by Maes are one such mechanism, which is quite popular. In general, it seems not possible to predict when behaviour networks are well-behaved. However, they perform quite well in the robotic soccer context. In this paper, we analyse the reason for this success by identifying conditions that make behaviour networks goal converging, i.e., force them to reach the goals …

Modular Answer Set Solving, Yuliya Lierler, Miroslaw Truszczyński

Yuliya Lierler

Modularity is essential for modeling large-scale practical applications.We propose modular logic programs as a modular version of answer set programming and study the relationship of our formalism to an earlier concept of lp-modules.

Weighted-Sequence Problem: Asp Vs Casp And Declarative Vs Problem-Oriented Solving, Yuliya Lierler, Shaden Smith

Yuliya Lierler

Search problems with large variable domains pose a challenge to current answer-set programming (ASP) systems as large variable domains make grounding take a long time, and lead to large ground theories that may make solving infeasible. To circumvent the “grounding bottleneck” researchers proposed to integrate constraint solving techniques with ASP in an approach called constraint ASP (CASP). In the paper, we evaluate an ASP system clingo and a CASP system clingcon on a handcrafted problem involving large integer domains that is patterned after the database task of determining the optimal join order. We find that search methods used by clingo …

Experiments With Sat-Based Answer Set Programming, Enrico Giunchiglia, Yuliya Lierler, Marco Maratea, A. Tacchella

Yuliya Lierler

Answer Set Programming (ASP) emerged in the late 1990s as a new logic programming paradigm which has been successfully applied in various application domains. Propositional satisfiability (SAT) is one of the most studied problems in Computer Science. ASP and SAT are closely related: Recent works have studied their relation, and efficient SAT-based ASP solvers (like assat and Cmodels) exist. In this paper we report about (i) the extension of the basic procedures in Cmodels in order to incorporate the most popular SAT reasoning strategies, and (ii) an extensive comparative analysis involving also other state-of-the-art answer set solvers. The experimental analysis …

Cmodels – Sat-Based Disjunctive Answer Set Solver, Yuliya Lierler

Yuliya Lierler

Disjunctive logic programming under the stable model semantics [GL91] is a new methodology called answer set programming (ASP) for solving combinatorial search problems. This programming method uses answer set solvers, such as DLV [Lea05], GNT [Jea05], SMODELS [SS05], ASSAT [LZ02], CMODELS [Lie05a]. Systems DLV and GNT are more general as they work with the class of disjunctive logic programs, while other systems cover only normal programs. DLV is uniquely designed to find the answer sets for disjunctive logic programs. On the other hand, GNT first generates possible stable model candidates and then tests the candidate on the minimality using system …

Sat-Based Answer Set Programming, Yuliya Lierler

Yuliya Lierler

Answer set programming (ASP) is a declarative programming paradigm oriented towards difficult combinatorial search problems. Syntactically, ASP programs look like Prolog programs, but solutions are represented in ASP by sets of atoms, and not by substitutions, as in Prolog. Answer set systems, such as SMODELS, SMODELSCC, and DLV, compute answer sets of a given program in the sense of the answer set (stable model) semantics. This is different from the functionality of Prolog systems, which determine when a given query is true relative to a given logic program. ASP has been applied to many areas of science and technology, from …

Computing Answer Sets Of A Logic Program Via-Enumeration Of Sat Certificates, Yuliya Lierler, Marco Maratea

Yuliya Lierler

Answer set programming is a new programming paradigm proposed based on the answer set semantics of Prolog. It is well known that an answer set for a logic program is also a model of the program's completion. The converse is true when the logic program is "tight". Lin and Zhao showed that for non-tight programs the models of completion which do not correspond to answer sets can be eliminated by adding to the completion what they called "loop formulas". Nevertheless, their solver ASSAT 1 has some disadvantages: it can work only with basic rules, and it can compute only one …

Cmodels: Sat-Based Answer Set Programming System, Yuliya Lierler, Marco Maratea

Yuliya Lierler

CMODELS [1, 2] is an answer set programming [3] system that uses the same frontend LPARSE as answer set solver SMODELS (http://www.tcs.hut.fi/Software/smodels/). CMODELS main computational characteristics is that it computes answer sets using a SAT solver for search. The use of SAT solvers for generating answer sets is based on the fact that for logic programs satisfying syntactic condition, tightness, the answer set semantics is equivalent to the Clark’s completion semantics. In addition, [4] introduced concept of a loop formula, and demonstrated that the answer sets of a logic program are exactly the models of its completion that satisfy the …

Abstract Answer Set Solvers With Backjumping And Learning, Yuliya Lierler

Yuliya Lierler

Nieuwenhuis et al. (2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937977 showed how to describe enhancements of the Davis–Putnam–Logemann–Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for several algorithms that generate answer sets for logic programs: SMODELS, SMODELS_cc, asp-sat with Learning (CMODELS), and a newly designed and implemented algorithm sup. This approach to describe answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.

Cmodels-2: Sat-Based Answer Set Solver Enhanced To Non-Tight Programs, Yuliya Lierler, Marco Maratea

Yuliya Lierler

Answer set programming is a new programming paradigm proposed in [1] and [2], and based on the answer set semantics of Prolog [3]. It is well known that an answer set for a logic program is also a model of the program’s completion [4]. The converse is true when the logic program is “tight” [6, 5]. Lin and Zhao [7] showed that for non-tight programs the models of completion which do not correspond to answer sets can be eliminated by adding to the completion what they called “loop formulas”. Nevertheless, their solver ASSAT1 has some disadvantages: it can work only …

Surviving Solver Sensitivity: An Asp Practitioner’S Guide, Bryan Silverthorn, Yuliya Lierler, Marius Schneider

Yuliya Lierler

Answer set programming (ASP) is a declarative programming formalism that allows a practitioner to specify a problem without describing an algorithm for solving it. In ASP, the tools for processing problem specifications are called answer set solvers. Because specified problems are often NP complete, these systems often require significant computational effort to succeed. Furthermore, they offer different heuristics, expose numerous parameters, and their running time is sensitive to the configuration used. Portfolio solvers and automatic algorithm configuration systems are recent attempts to automate the problem of manual parameter tuning, and to mitigate the burden of identifying the right solver configuration. …