Constraint Answer Set Programming

By
Yuliya Lierler
University of Nebraska at Omaha

We are greatful to Marcello Balduccini, Broes de Cat, Vladimir Lifschitz, and Peter Schüller for valuable comments.

PDF Version

Introduction

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 programming, and nonmonotonic reasoning. As a declarative programming paradigm, it provides a rich, simple modeling language that, among other features, incorporates recursive definitions. Answer set programming languages also use variables; software tools called grounders are used as front ends of answer set solvers to eliminate variables, whereas SAT-like procedures form their back-ends.

Constraint answer set programming draws on both of these extensions of SAT technology: it integrates answer set programming with constraint processing.

This new area has already demonstrated promising results, including the development of the CASP solvers acsolver [11] (Texas Tech University), clingcon [7] (Potsdam University, Germany), ezcsp [1] (KODAK), idp [15] (KU Leuven), mingo [10] (Aalto University, Finland). CASP is a new, powerful paradigm for declarative programming that provides new modeling features for answer set programming and also improves grounding and solving performance by delegating processing of constraints over large and possibly infinite domains to specialized systems. As a result CASP opens new horizons for declarative programming applications. The origins of this work go back to [2].

Related Work: HEX-Programs [3] integrate logic programs under answer set semantics with external computation sources via external atoms. They were motivated by the need to interface ASP with external computation sources, for example, to allow the synergy of ASP and description logic computations within the context of the semantic web. CASP shares a lot in common with HEX-programs. System dlvhex⁵ [4] computes models of such programs. It allows defining plug-ins for inference on external atoms and as such can be used as a general framework for developing CASP solvers (but it does not provide any specific computational mechanism by default).

1 Logic Programs with Constraint Atoms

A regular program is a finite set of rules of the form

(1)

where a₀ is ⊥ or an atom, and each a_i (1 ≤ i ≤ n) is an atom. This is a special case of programs with nested expressions [9]. We refer the reader to the paper by Lifschitz et al.[9] for details on the definition of an answer set of a logic program. A choice rule construct {a} [12] of the lparse language can be seen as an abbreviation for a rule a ← not not a [5]. We adopt this abbreviation in the rest of the paper.

A constraint satisfaction problem (CSP) is defined as a triple ⟨X,D,C⟩, where X is a set of variables, D is a domain of values, and C is a set of constraints. Every constraint is a pair ⟨t,R⟩, where t is an n-tuple of variables and R is an n-ary relation on D. An evaluation of the variables is a function from the set of variables to the domain of values, ν : X → D. An evaluation ν satisfies a constraint ⟨(x₁,…,x_n),R⟩ if (v(x₁),…,v(x_n)) ∈ R. A solution is an evaluation that satisfies all constraints.

Consider an alphabet consisting of regular and constraint atoms, denoted by A and C respectively. By C~ we denote the set of all literals over C. The constraint literals are identified with constraints via a function γ : C~→ C so that for any literal l, γ(l) has a solution if and only if γ(-l) does not have one (where -l denotes a complement of l). For a set Y of constraint literals over C, by γ(Y ) we denote a set of corresponding constraints, i.e., {γ(c)|c ∈ Y }. Furthermore, each variable in γ(C~) is associated with a domain. For a set M of literals, by M⁺ and M^C we denote the set of positive literals in M and the set of constraint literals over C in M, respectively.

A logic program with constraint atoms is a regular logic program over an extended alphabet A ∪ C such that a₀ is ⊥ or a₀ ∈ A. Given a logic program with constraint atoms Π, by Π^C we denote Π extended with choice rules {c} for each constraint atom c occurring in Π. We say that a consistent and complete set M of literals over atoms of Π is an answer set of Π if (i) M⁺ is an answer set of Π^C and (ii) γ(Π^C) has a solution.

For example, let Π be the program (2)

am <- X < 12

lightOn <- switch, not am

{switch}

⊥ <- not lightOn

Intuitively, this program states that (a) light is on only if an action of switch occurs during the pm hours and (b) light is on (according to the last rule in the program). Consider a domain of X to be integers from 0 till 24. It is easy to see that a set   forms the only answer set of program (2).

2 On the relation of constraint answer set languages and solvers

In the introduction, we listed a number of CASP systems acsolver, clingcon, ezcsp, idp, mingo that were developed in recent years. The core of the languages of these systems is captured by the definition of a logic program with constraint atoms presented here. Yet, relating these languages is not an easy task. One difficulty lies in the fact that these languages are introduced together with specific system archetecture in mind that rely on various ASP/CSP/CLP/SMT technology. The syntactic differences that stam from technological differences stand on the way of clear understanding of key features of the languages. Relating CASP systems formally is even more complex task. The variations in underlying technologies complicate clear articulation of their similarities and differences. For example, the CASP solver clingcon [7] is developed using an ASP solver clasp [6] and a constraint solver gecode [14]. The main building blocks of the CASP solver acsolver [11] are the ASP system smodels [12] and sicstus prolog⁶ . In addition, the CASP solvers adopt different communication schemes among their heterogeneous solving components. For instance, the system ezcsp relies on blackbox integration of ASP and CSP tools in order to compute the answer sets of an ezcsp program [1]. Systems acsolver, clingcon, idp promote tighter integration of multiple automated reasoning methods. The broad attention to CASP paradigms suggests a need for a principled and general study of methods to develop unifying terminology and formalisms suitable to capture variants of the languages and solvers. The work by Lierler [8] can be seen as a step in this direction. It presents a formal account that illustrates a precise relationship between the languages of acsolver and clingcon as well as between the respective systems. Usually backtrack search procedures (Davis-Putnam-Logemann-Loveland (DPLL)-like procedures) that form a backbone of CASP computational methods are described in terms of pseudocode. In [13], the authors proposed an alternative approach to describing DPLL-like algorithms. They introduced an abstract framework that captures what states of computation are, and what transitions between states are allowed. In this way, it defines a directed graph such that every execution of DPLL corresponds to a path in this graph. Some edges may correspond to a propagation steps, some to branching, some to backtracking. This approach allows us to model a DPLL-like algorithm by a mathematically simple and elegant object, graph, rather than a collection of pseudocode statements. An abstract framework of the sort served as the main tool for performing precise formal analyses relating such constraint answer set solvers as acsolver and clingcon [8].

References