{"id":2322,"date":"2012-09-30T00:00:43","date_gmt":"2012-09-30T06:00:43","guid":{"rendered":"http:\/\/www.cs.nmsu.edu\/ALP\/?p=2322"},"modified":"2012-10-02T14:22:08","modified_gmt":"2012-10-02T20:22:08","slug":"constraint-answer-set-programming","status":"publish","type":"post","link":"https:\/\/logicprogramming.org\/2012\/09\/constraint-answer-set-programming\/","title":{"rendered":"Constraint Answer Set Programming"},"content":{"rendered":"

By
\nYuliya Lierler<\/strong>
\nUniversity of Nebraska at Omaha<\/p>\n

We are greatful to Marcello Balduccini, Broes de Cat, Vladimir Lifschitz, and Peter Sch\u00fcller for valuable comments.<\/p>\n

PDF Version<\/a><\/p>\n

<\/a>Introduction<\/h3>\n

<\/p>\n

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.
\n<\/p>\n

Constraint answer set programming draws on both of these extensions of SAT technology: it integrates answer set programming with constraint processing.<\/p>\n

This new area has already demonstrated promising results, including the development of the CASP solvers a<\/span>c<\/span>s<\/span>o<\/span>l<\/span>v<\/span>e<\/span>r<\/span><\/span> [11<\/a>]<\/span> (Texas Tech University), c<\/span>l<\/span>i<\/span>n<\/span>g<\/span>c<\/span>o<\/span>n<\/span><\/span> <\/sup><\/a><\/span>[7<\/a>]<\/span> (Potsdam University, Germany), e<\/span>z<\/span>c<\/span>s<\/span>p<\/span><\/span> <\/sup><\/a><\/span>[1<\/a>]<\/span> (KODAK), i<\/span>d<\/span>p <\/span><\/span>[15<\/a>]<\/span> (KU Leuven), m<\/span>i<\/span>n<\/span>g<\/span>o <\/span><\/span>[10<\/a>]<\/span> (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\u00a0[2<\/a>]<\/span>.
\n<\/p>\n

Related Work: <\/span>HEX-Programs\u00a0[3<\/a>]<\/span> integrate logic programs under answer set semantics with external computation sources via external atoms<\/span>. 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 d<\/span>l<\/span>v<\/span>h<\/span>e<\/span>x<\/span><\/span>5<\/sup><\/a><\/span> [4<\/a>]<\/span> 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).<\/p>\n

1 <\/span> <\/a>Logic Programs with Constraint Atoms<\/h3>\n

<\/p>\n

A regular program <\/span>is a finite set of rules of the form<\/p>\n\n\n\n
\"a0<\/a><\/td>\n(1)<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

<\/p>\n

where a<\/span>0<\/span><\/sub> is \u22a5 <\/span>or an atom, and each a<\/span>i<\/span><\/sub> (1 \u2264 <\/span>i <\/span>\u2264 <\/span>n<\/span>) is an atom. This is a special case of programs with nested expressions [9<\/a>]<\/span>. We refer the reader to the paper by Lifschitz et al.[9<\/a>]<\/span> for details on the definition of an answer set of a logic program. A choice rule<\/span> <\/em>construct {<\/span>a<\/span>}<\/span> [12<\/a>]<\/span> of the l<\/span>p<\/span>a<\/span>r<\/span>s<\/span>e<\/span> <\/span>language can be seen as an abbreviation for a rule a <\/span>\u2190<\/span> not<\/span> not<\/span> a<\/span> [5<\/a>]<\/span>. We adopt this abbreviation in the rest of the paper.
\n<\/p>\n

A constraint satisfaction problem<\/em> (CSP) is defined as a triple \u27e8<\/span>X,D,C<\/span>\u27e9<\/span>, where X<\/span> is a set of variables, D <\/span>is a domain of values, and C <\/span>is a set of constraints. Every constraint is a pair \u27e8<\/span>t,R<\/span>\u27e9<\/span>, where t <\/span>is an n<\/span><\/em>-tuple of variables and R <\/span>is an n<\/span>-ary relation on D<\/span>. An evaluation <\/span>of the variables is a function from the set of variables to the domain of values, \u03bd <\/span>: X <\/span>\u2192 <\/span>D<\/span>. An evaluation\u00a0\u03bd <\/em><\/span>satisfies<\/em> <\/span>a constraint \u27e8<\/span>(x<\/span>1<\/span><\/sub>,<\/span>\u2026<\/span>,x<\/span>n<\/span><\/sub>),R<\/span>\u27e9 <\/span>if (v<\/span>(x<\/span>1<\/span><\/sub>),<\/span>\u2026<\/span>,v<\/span>(x<\/span>n<\/span><\/sub>)) \u2208 <\/span>R<\/span>. A solution<\/em> <\/span>is an evaluation that satisfies all constraints.
\n<\/p>\n

Consider an alphabet consisting of regular and constraint atoms, denoted by A<\/em><\/strong> and C<\/em><\/strong> <\/span>respectively. By C~<\/strong> we denote the set of all literals over C<\/strong>. The constraint literals are identified with constraints via a function \u03b3 <\/span>: C~<\/strong>\u2192 <\/span>C<\/strong> <\/span>so that for any literal l<\/span>, <\/span>\u03b3(l<\/span>) has a solution if and only if \u03b3(-l<\/span><\/span>) does not have one (where -l<\/span><\/span> denotes a complement of l<\/span>). For a set Y <\/span>of constraint literals over C,<\/strong> by \u03b3<\/span>(Y <\/span>) we denote a set of corresponding constraints, i.e., {<\/span>\u03b3<\/span>(c<\/span>)|<\/span>c <\/span>\u2208 <\/span>Y <\/span>}<\/span>. Furthermore, each variable in \u03b3<\/span>(C~<\/strong>) is associated with a domain. For a set M <\/span>of literals, by\u00a0M<\/span>+<\/span><\/sup> and M<\/span>C<\/sup> we denote the set of positive literals in <\/span>M and the set of constraint literals over <\/span>C <\/strong>in <\/span>M, respectively.<\/span>
\n<\/p>\n

A logic program with constraint atoms <\/span>is a regular logic program over an extended alphabet A<\/strong> \u222a <\/span>C <\/strong> <\/span>such that a<\/span>0<\/span><\/sub> is \u22a5 <\/span>or a<\/span>0<\/span><\/sub> \u2208 A<\/strong><\/span>. Given a logic program with constraint atoms \u03a0, by \u03a0C<\/sup> we denote <\/span>\u03a0 extended with choice rules {<\/span>c<\/span>} <\/span>for each constraint atom c <\/span>occurring in \u03a0. We say that a consistent and complete set M <\/span>of literals over atoms of \u03a0 is an answer set of \u03a0 if (i) M<\/span>+<\/span><\/sup> is an answer set of \u03a0C <\/sup>and<\/span> (ii<\/span>) \u03b3<\/span>(\u03a0C<\/sup><\/sup>) has a solution.<\/span>
\n<\/p>\n

For example, let \u03a0 be the program (2)<\/p>\n

am <- X < 12<\/pre>\n
lightOn <- switch, not am<\/pre>\n
{switch}<\/pre>\n
\u22a5 <- not lightOn<\/pre>\n
Intuitively, this program states that (a) light <\/span>is on <\/span>only if an action of switch <\/span>occurs during the pm <\/span>hours and (b) light <\/span>is on <\/span>(according to the last rule in the program). Consider a domain of X <\/span>to be integers from 0 till 24. It is easy to see that a set\u00a0\u00a0 \"{switch,lightOn,\u00ac forms the only answer set of program\u00a0(2<\/a>).<\/p>\n
<\/p>\n
\n
2 <\/span> <\/a>On the relation of constraint answer set languages and solvers<\/h3>\n
<\/p>\n
In the introduction, we listed a number of CASP systems a<\/span>c<\/span>s<\/span>o<\/span>l<\/span>v<\/span>e<\/span>r<\/span><\/span>, c<\/span>l<\/span>i<\/span>n<\/span>g<\/span>c<\/span>o<\/span>n<\/span><\/span>, e<\/span>z<\/span>c<\/span>s<\/span>p<\/span><\/span>, i<\/span>d<\/span>p<\/span><\/span>, m<\/span>i<\/span>n<\/span>g<\/span>o<\/span> <\/span>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 c<\/span>l<\/span>i<\/span>n<\/span>g<\/span>c<\/span>o<\/span>n<\/span><\/span> [7<\/a>]<\/span> is developed using an ASP solver c<\/span>l<\/span>a<\/span>s<\/span>p<\/span><\/span> [6<\/a>]<\/span> and a constraint solver g<\/span>e<\/span>c<\/span>o<\/span>d<\/span>e<\/span> <\/span>[14<\/a>]<\/span>. The main building blocks of the CASP solver a<\/span>c<\/span>s<\/span>o<\/span>l<\/span>v<\/span>e<\/span>r<\/span><\/span> [11<\/a>]<\/span> are the ASP system s<\/span>m<\/span>o<\/span>d<\/span>e<\/span>l<\/span>s<\/span> <\/span>[12<\/a>]<\/span> and s<\/span>i<\/span>c<\/span>s<\/span>t<\/span>u<\/span>s<\/span><\/span> p<\/span>r<\/span>o<\/span>l<\/span>o<\/span>g<\/span><\/span>6<\/sup><\/a><\/span> . In addition, the CASP solvers adopt different communication schemes among their heterogeneous solving components. For instance, the system e<\/span>z<\/span>c<\/span>s<\/span>p<\/span> <\/span>relies on blackbox <\/span>integration of ASP and CSP tools in order to compute the answer sets of an e<\/span>z<\/span>c<\/span>s<\/span>p<\/span> <\/span>program\u00a0[1<\/a>]<\/span>. Systems a<\/span>c<\/span>s<\/span>o<\/span>l<\/span>v<\/span>e<\/span>r<\/span><\/span>, c<\/span>l<\/span>i<\/span>n<\/span>g<\/span>c<\/span>o<\/span>n<\/span><\/span>, i<\/span>d<\/span>p<\/span> <\/span>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\u00a0[8<\/a>]<\/span> can be seen as a step in this direction. It presents a formal account that illustrates a precise relationship between the languages of a<\/span>c<\/span>s<\/span>o<\/span>l<\/span>v<\/span>e<\/span>r<\/span> <\/span>and c<\/span>l<\/span>i<\/span>n<\/span>g<\/span>c<\/span>o<\/span>n<\/span> <\/span>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\u00a0[13<\/a>]<\/span>, 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 a<\/span>c<\/span>s<\/span>o<\/span>l<\/span>v<\/span>e<\/span>r<\/span> <\/span>and c<\/span>l<\/span>i<\/span>n<\/span>g<\/span>c<\/span>o<\/span>n<\/span><\/span> [8<\/a>]<\/span>.<\/p>\n
<\/a>References<\/h3>\n
<\/p>\n
\n
\n

\n[1] <\/span><\/span>Marcello Balduccini.  Representing constraint satisfaction problems in answer set programming. In Proceedings of ICLP\u201909 Workshop on Answer<\/span> Set Programming and Other Computing Paradigms (ASPOCP\u201909)<\/span>, 2009.<\/p>\n

\n[2] <\/span><\/span>Sabrina Baselice, Piero\u00a0A. Bonatti, and Michael Gelfond. Towards an integration of answer set and constraint solving. In Maurizio Gabbrielli and Gopal Gupta, editors, ICLP<\/span>, volume 3668 of Lecture Notes in Computer<\/span> Science<\/span>, pages 52\u201366. Springer, 2005.<\/p>\n

\n[3] <\/span><\/span>Thomas                                                                           Eiter, Gerhard  Brewka,  Minh  Dao-Tran,  Michael  Fink,  Giovambattista  Ianni, and Thomas Krennwallner.  Combining Nonmonotonic Knowledge Bases with External Sources. In Silvio Ghilardi and Roberto Sebastiani, editors, 7th International Symposium on Frontiers of Combining Systems (FroCos<\/span> 2009)<\/span>, volume 5749 of LNAI<\/span>, pages 18\u201342. Springer, September 2009.<\/p>\n

\n[4] <\/span><\/span>Thomas Eiter, Giovambattista Ianni, Roman Schindlauer, and Hans Tompits.   A uniform integration of higher-order reasoning and external evaluations in answer set programming.  In Proceedings of International<\/span> Joint Conference on Artificial Intelligence (IJCAI)<\/span>, pages 90\u201396, 2005.<\/p>\n

\n[5] <\/span><\/span>Paolo Ferraris and Vladimir Lifschitz.   Weight constraints as nested expressions. Theory and Practice of Logic Programming<\/span>, 5:45\u201374, 2005.<\/p>\n

\n[6] <\/span><\/span>Martin Gebser, Benjamin Kaufmann, Andre Neumann, and Torsten Schaub.    Conflict-driven  answer  set  solving.    In  Proceedings  of  20th<\/span> International Joint Conference on Artificial Intelligence (IJCAI\u201907)<\/span>, pages 386\u2013392. MIT Press, 2007.<\/p>\n

\n[7] <\/span><\/span>Martin Gebser, Max Ostrowski, and Torsten Schaub. Constraint answer set  solving.   In  Proceedings  of  25th  International  Conference  on  Logic<\/span> Programming (ICLP)<\/span>, pages 235\u2013249. Springer, 2009.<\/p>\n

\n[8] <\/span><\/span>Yuliya Lierler.  On the relation of constraint answer set programming languages  and  algorithms.   In  Proceedings of the AAAI Conference on<\/span> Artificial Intelligence<\/span>. MIT Press, 2012.<\/p>\n

\n[9] <\/span><\/span>Vladimir  Lifschitz,  Lappoon\u00a0R.  Tang,  and  Hudson  Turner.   Nested expressions  in  logic  programs.    Annals  of  Mathematics  and  Artificial<\/span> Intelligence<\/span>, 25:369\u2013389, 1999.<\/p>\n

\n[10] <\/span><\/span>Guohua  Liu,  Tomi  Janhunen,  and  Ilkka  Niemelae.     Answer  set programming via mixed integer programming. In Principles of Knowledge<\/span> Representation  and  Reasoning:  Proceedings  of  the  13th  International<\/span> Conference<\/span>, page 3242, 2012.<\/p>\n

\n[11] <\/span><\/span>Veena\u00a0S. Mellarkod, Michael Gelfond, and Yuanlin Zhang. Integrating answer  set  programming  and  constraint  logic  programming.   Annals of<\/span> Mathematics and Artificial Intelligence<\/span>, 2008.<\/p>\n

\n[12] <\/span><\/span>Ilkka Niemel\u00e4 and Patrik Simons. Extending the Smodels system with cardinality and weight constraints.  In Jack Minker, editor, Logic-Based<\/span> Artificial Intelligence<\/span>, pages 491\u2013521. Kluwer, 2000.<\/p>\n

\n[13] <\/span><\/span>Robert          Nieuwenhuis,          Albert          Oliveras,          and Cesare Tinelli.  Solving SAT and SAT modulo theories: From an abstract
\nDavis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the<\/span> ACM<\/span>, 53(6):937\u2013977, 2006.<\/p>\n

\n[14] <\/span><\/span>Christian Schulte and Peter\u00a0J. Stuckey. Efficient constraint propagation engines. Transactions on Programming Languages and Systems<\/span>, 2008.<\/p>\n

\n[15] <\/span><\/span>Johan Wittocx, Maarten Mari\u00ebn, and Marc Denecker. The i<\/span>d<\/span>p<\/span> <\/span>system: a model expansion system for an extension of classical logic.   In Marc Denecker, editor, LaSh<\/span>, pages 153\u2013165, 2008.<\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"
By Yuliya Lierler,
\nUniversity of Nebraska at Omaha<\/p>\n
Read more →<\/a><\/p>\n","protected":false},"author":5,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[3,5],"tags":[],"class_list":["post-2322","post","type-post","status-publish","format-standard","hentry","category-issue","category-articles"],"_links":{"self":[{"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/posts\/2322","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/users\/5"}],"replies":[{"embeddable":true,"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/comments?post=2322"}],"version-history":[{"count":14,"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/posts\/2322\/revisions"}],"predecessor-version":[{"id":2370,"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/posts\/2322\/revisions\/2370"}],"wp:attachment":[{"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/media?parent=2322"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/categories?post=2322"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/logicprogramming.org\/wp-json\/wp\/v2\/tags?post=2322"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}