An ASP Semantics for Default Reasoning with Constraints

1 Introduction

Although Answer Set Programming (ASP; [Lifschitz, 2008]) has become a prime candidate for knowledge representation and reasoning, it falls short of succinctly representing variables over large numeric domains. So far, this was addressed by hybridizing ASP with Constraint Processing (CP; [Dechter, 2003]), leading to the subarea of Constraint ASP (CASP; [Lierler, 2014]). In fact, the design of most CASP approaches is inspired by the algorithmic framework of Satisfiability modulo Theories (SMT; [Nieuwenhuis et al., 2006]) and thus leads to hybrid semantics combining nonmonotonic aspects of ASP with monotonic ones of CP. This yields an inevitable blind spot, namely, the incapacity of providing defaults for constraint variables (or even leaving them undefined). Such features must be addressed on the ASP side, which brings us back to the aforementioned problem.

We address this dilemma by introducing a new approach that integrates ASP and CP in the uniform semantic framework of the logic of Here-and-There (HT; [Heyting, 1930]), extending the Equilibrium Logic [Pearce, 1997] characterization of ASP to theories with constraint atoms. This puts both ASP and CP on the same semantic footing, being nonmonotonic in nature. The new logic of Here-and-There with constraints, HTC for short, is built from variables over associated domains, whose valid valuations are determined by the interpretation of constraint atoms. HTC is not only a proper generalization of HT, and hence also ASP, but it also tolerates undefined constraint variables and lets them take default values. Moreover, the logic programming fragment of HTC also subsumes the CASP approach of [Gebser et al., 2009]. Interestingly, the monotonic nature of constraint variables in CASP can be obtained by adding simple axioms, similar to tertium non datur in HT (or choice rules in ASP). Finally, we elaborate upon the fragment of logic programs with linear constraints on integer variables, LC, and introduce directional assignments in rule heads in order to guarantee foundedness in the presence of undefinedness. Furthermore, we develop a translation of LC-programs into CASP that forms the backbone of our implementation by means of off-the-shelf CASP solvers.

2 Here-and-There with Constraints

In this section, we introduce the logic of Here-and-There with Constraints, HTC for short.

We begin by recalling the definition of a constraint satisfaction problem as a triple hX↪D↪ Ci where X is a set of variables, D a domain of values, and C a set of constraints. Each constraint is a pair hx↪ Ri where x is an n-tuple of variables and R an n-ary relation on D. A valuation of the variables is a function from the set of variables to the domain of values v : X ! D. A valuation v satisfies a constraint h(x1↪ ▷ ▷ ▷ ↪ xn)↪Ri if (v(x1)↪ ▷ ▷ ▷ ↪ v(xn)) 2 R. A solution of hX↪D↪ Ci is a valuation v that satisfies all constraints in C.

The syntax of HTC starts from a similar signature hX↪D↪Ai where, as before, X are variables and D domain values, but A are now constraint atoms, or just atoms for short. The syntax of a constraint atom is left open and depends on the respective type of constraints. We assume that it always has a set of associated variables from X and sometimes refers to elements in D. Examples of constraint atoms are x + y  3, x = y, all di↵ (¶x↪ y↪ z♦), or x 2 ¶t↪ f♦ where x↪ y↪ z are variables and 3↪ t↪ f are values. We sometimes refer to a subset of variables P ✓ X as propositions and let the subset ¶t↪ f♦ ✓ D of values stand for Boolean truth values. Also, for each proposition p 2 P, we include a constraint atom (p = t) 2 A that we call regular atom and usually abbreviate by p. We also allow for atoms of form (p = f) 2 A, standing for the strong negation of p, and alternatively write them as ⇠p. A formula is any propositional combination of atoms and logical connectives ?↪ ^↪ _↪!.

We define negation as ≻' def = ' ! ? and double implication as '$ def = ('! ) ^ ( !').

Satisfaction of formulas is defined wrt a fixed function, called atom denotation, J · K : A ! 2V that maps each atom to a closed set of partial valuations. As examples of atom denotations, we have the following:

The semantics of HTC is defined as follows. A partial valuation v is a function v : X ! D [ ¶u♦ assigning to each variable in X either a domain value from D or the special value u 62 D standing for "undefined." A partial valuation can be alternatively represented as a set v ✓ X ⇥D that does not contain two different pairs (x↪ c) and (x↪ d) with c 6= d for the same variable x and that does not include any pair (x↪ ·) when v(x) = u. With this set representation, we use the standard ✓ relation to compare partial evaluations. We define VX↪D as the set of all possible partial valuations for X and D and remove the subindices when clear from the context. We use letters v↪ v0 to denote elements of V. The closure of a set S of partial valuations is defined as S " def = ¶v ♣ v ◆ v0 ↪ v0 2 S♦. A set S of partial valuations is said to be closed if S " = S. Given two variables x↪ y 2 X and a domain D = ¶1↪ 2♦, an example of a non-closed set of valuations is ¶v 2 V ♣ v(x) = v(y)♦ since v = ; satisfies v(x) = v(y) = u but its superset v0 = ¶(x↪ 1)↪ (y↪ 2)♦ does not satisfy v0 (x) = v0 (y). On the other hand, ¶v 2 V ♣ v(x) = v(y) 6= u♦ is closed.

= ¶A 2 A ♣ v 2 JAK♦ or At(v) for short. Proposition 1 Let v ✓ v0 be a pair of partial valuations and J · K a denotation for atoms in A. Then At(v) ✓ At(v0 ). The denotation for regular atoms is fixed as expected:

J some zero(x↪ y) K def As mentioned, denotations must be closed. For instance, all above examples satisfy JAK" = JAK. This property allows us to prove the following result. Given a denotation J · K and a partial valuation v, we define the set of atoms that hold in v as AtJ · K(v) def

J ⇠p K = J p = f K def Let X = ¶x1↪ ▷ ▷ ▷ ↪ xn♦ be a subset of variables X ✓ X. A constraint C = h(x1↪ ▷ ▷ ▷ ↪ xn)↪ Ri can be understood as the following set of partial valuations:

These are all valuations fixing variables in X to some tuple in R while varying the remaining variables X ∩ X in all possible ways (including being undefined). Notice that v(xi) is always defined for all variables in X and any valuation v in the constraint. A set of partial valuations is said to be strict if it corresponds to some constraint C. Otherwise, it is said to be non-strict. For instance, the denotation Jx = y K provided before is strict because we can represent it as a constraint h(x↪ y)↪Ri where R = ¶(d↪ d) ♣ d 2 D♦. However, J some zero(x · y) K is non-strict because we may have v(x) = 0 but v(y) undefined or the other way around. This cannot be captured by a constraint: we cannot cover this set of valuations as any h(x↪ y)↪ Ri, h(x)↪ Ri or h(y)↪ Ri because we must include both v1 = ¶(x↪ 0)♦, where y is undefined, and v2 = ¶(y↪ 0)♦, where x is undefined. In this paper, we focus on strict denotations for atoms.

An interpretation in HTC is a pair hH↪ Ti of partial valuations such that H ✓ T .

Definition 1 Given a fixed denotation J · K, we say that an interpretation hH↪ T i satisfies a formula ', written hH↪ T i ♣= ', when the following recursive conditions hold:

• (i) hH↪ Ti ♣= A iff H 2 JAK (ii) ?↪ _↪ ^ as usual
• (iii) hH↪ Ti ♣= ' ! iff for both v = H and v = T it holds: hv↪ Ti 6♣= ' or hv↪ Ti ♣= .

As usual, an interpretation hH↪ T i is a model of a theory Γ, written hH↪ Ti ♣= Γ, if it satisfies all formulas in Γ, that is, hH↪ Ti ♣= ' for all ' 2 Γ. A theory (or a single formula) Γ entails a formula ', written Γ ♣= ', when all models of Γ are models of '. We write ' ⌘ to represent that ' and are equivalent, that is, have the same HTC models.

Observation 1 The logic of Here-and-There can be obtained as a case of HTC with a signature hX ↪ D↪ Ai where X represents propositions, D = ¶t♦ and A = X , understanding each p 2 A as an abbreviation of the constraint atom (p = t) as explained above. Moreover, this can be generalized to any arbitrary singleton D = ¶d♦ and corresponding constraint atoms (p = d) and the relationship still holds.

The following is an interesting connection between HTC and HT :

Proposition 2 Let Γ be some HTC theory for signature hX↪D↪Ai and let hH↪ Ti be some model of Γ. Then, hAt(H)↪At(T)i is an HT model of Γ under signature hA↪ ¶t♦↪ ¶p = t ♣ p 2 A♦i. 1

As a result, we directly derive these properties from HT:

Proposition 3 For any formula ':

• ÷ hH↪ Ti ♣= ' implies hT↪ Ti ♣= '
• ÷ hH↪ Ti ♣= ≻' iff hT↪ Ti 6♣= '
• ÷ Any tautology in HT is also a tautology in HTC.

In the light of Proposition 2, one might wonder whether, to capture HTC semantics, it would suffice to exclusively consider HT theories built with constraint atoms used as propositional variables without entering into their internal semantics. This is not the case, since we cannot obtain a similar correspondence in the opposite direction. Namely, not any arbitrarily chosen pair of sets of atoms H0 ✓ T 0 ✓ A necessarily corresponds to an HTC interpretation hH↪ Ti such that H0 = At(H) and T 0 = At(T). As an example, take H0 = ¶x = y♦ ⇢ ¶x = y↪ x = 0♦ = T 0 . Clearly, to obtain At(T) = T 0 we need T = ¶(x↪ 0)↪ (y↪ 0)♦. Now, the only subset of T that satisfies x = y is H = T itself. But then At(H) = At(T ) = T 0 6= H0 .

1 Or simply hA↪ ¶t♦↪ Ai by abbreviating all (p = t) by p.

We sometimes write T ♣= ' to stand for hT↪ Ti ♣= '. Extending the equilibriummodel definition [Pearce, 1997] to HTC theories is straightforward.

Definition 2 An interpretation hT↪ Ti is an equilibrium model of a theory Γ if hT↪ Ti ♣= Γ and there is no H ⇢ T such that hH↪ Ti ♣= Γ.

In this case, we also say that T is a stable model of Γ. Again, if we restrict the signature to hA↪ ¶t♦↪ Ai, we obtain standard equilibrium/stable models.

For logic programming syntax, we use comma '↪' and semicolon ';' as alternative representations of ^ and _, respectively. Similarly, we write ' to stand for !', as expected. An HTC-literal is an atom A or its default negation ≻A. An HTC program is a set of rules of the form:

where each Li is an HTC-literal.

Example 1 For solving the 8-queens puzzle, we define the variables X = ¶q1↪ ▷ ▷ ▷ ↪ q8♦ where qi represents the column of the queen located at row i. We are given some queens already placed and, by default, the first queen should be located at column 1. A possible way to encode this problem is as follows. We use the domain values D = ¶1↪ ▷ ▷ ▷ ↪ 8♦ and use the atoms all di↵ (X) and ♣x-y♣ = d as given above. Then, we specify the problem as the HTC-program ⇧1:

where i↪ j↪ k 2 D, i 6= j, k > 1 and di↪j is the constant ♣i-j♣. Without further information, the program ⇧1 yields four solutions corresponding to the possible 8-queens arrangements with q1 = 1. However, if we add the fact q1 = 4, we obtain the 18 possible solutions where queen 1 is located at row 4.

As we can see, constraints can be used to encode default reasoning, such as the default value 1 for variable q1 in the example. This feature of HTC cannot be represented with the usual semantics for CASP [Gebser et al., 2009] which separates regular ASP atoms (that allow for defaults) from constraint atoms, that only permit monotonic reasoning. As a result, any CASP program that does not contain regular atoms is monotonic. Note the difference wrt HTC where, due to Observation 1, it is always possible to encode any standard logic program only using constraint variables and picking an arbitrary singleton domain. For instance, the ASP program ¶p ≻q♦ can be directly encoded as ¶p = 1 ≻(q = 1)♦ using integer variables instead of Boolean atoms.

Capturing CASP constraints in HTC can be easily achieved. Take the following pair of axioms:

A variable x is said to be defined (resp. rigid) in a theory Γ if the axiom (5) (resp. (6)) is entailed by Γ.

Proposition 4 For any model hH↪ Ti of Γ:

• ÷ If x is defined in Γ, then T(x) 6= u
• ÷ If x is rigid in Γ, then H(x) = T(x)

Intuitively, (5) acts as a constraint forbidding stable models with x undefined. However, x can be undefined in H, that is, during models minimization. Thus, a defined variable may be assigned a default value, as we did with q1 in Example 1. On the other hand, (6) forces a monotonic behavior for x, so that we can freely choose its value beforehand, including the case in which we decide to leave it undefined. When a variable is both defined and rigid it satisfies (5) and (6), whose conjunction amounts to the axiom x = x. This axiom acts as a choice rule allowing to pick any arbitrary value in D for x.

Theorem 1 The definition of CASP provided in [Gebser et al., 2009] exactly corresponds to HTC programs where all variables are defined and rigid.

In fact, we can apply this same technique (adding axiom x = x) to selectively fix a CASP behavior only for some variable x. This is analogous to the addition of the ASP choice 2 p _ ≻p to make proposition p behave classically.

3 Logic programs with Linear Constraints

In this section, we focus on a family of constraint atoms for dealing with linear constraints on integer variables, studying some useful syntactic constructions for logic programs with this kind of atoms. A linear constraint is a constraint atom of the form ↵  β where ↵ and β are in their turn linear expressions defined as follows. A linear expression ↵ is a sum t1 + · · · + tn where each addend ti can be a product di · xi or simply a constant di, being di 2 Z and xi 2 X. By Vars(↵) we denote the set of variables occurring in ↵ and we sometimes write Vars(↵↪ β) def = Vars(↵) [ Vars(β) when dealing with two linear expressions. A linear constraint ↵  β is said to be in normal form if β = d 2 Z. We adopt some usual abbreviations. We simply write xi instead of 1 · xi and we directly replace the '+' symbol by '-' for negative constants. Moreover, when clear from the context, we sometimes omit the '·' symbol. As an example, -x+3 y2 z stands for (-1) · x + 3 · y + (-2) · z. Other abbreviations must be handled with care. In particular, we neither remove products of form 0 · x nor replace them by 0.

To define the denotation of a linear constraint, we extend any partial valuation v on integer variables to any arbitrary arithmetic term t in the following way:

for any variable x 2 X and any operator ⊕ 2 ¶·↪+♦. As before, we write v(t) = u to represent that v(t) is undefined.

2 This HT-formula is frequently denoted as ¶p♦ in ASP.

In other words, an arithmetic expression is evaluated as usual, except that it is undefined if it contains some undefined subterm (or eventually, some undefined variable).

Proposition 5 For any arithmetic expression t and HTC interpretation hH↪ T i, H(t) 6= u implies H(t) = T (t).

The denotation of a linear constraint ↵  β is defined as:

J ↵  β K def = ¶v ♣ v(↵)↪ v(β) 2 Z↪ v(↵)  v(β)♦ This collects interpretations assigning some integer both to ↵ and β, and additionally v(↵)  v(β). Therefore, ↵  β does not hold in interpretations where some variable in Vars(↵↪ β) is undefined (or assigned a non-integer value). We can also observe that J↵  β K is strict, since it can be represented as the constraint h(x1↪ ▷ ▷ ▷ ↪ xn)↪ Ri with Vars(↵↪ β) = ¶x1↪ ▷ ▷ ▷ ↪ xn♦ and R containing all the n-tuples of integer values that assigned to the variables fulfill v(↵)  v(β).

We use some abbreviations: we write ↵ = β to stand for the conjunction 3 ↵  β ^ β  ↵. Given an inequality A : (↵  β), we write A to stand for (β < ↵) def = β  ↵^≻(↵  β). We also define the formula ↵ 6= β as ↵ < β _ β < ↵. Notice that ↵ 6= β is stronger than ≻(↵ = β) since the former requires ↵ and β to have different values (and so, to be both defined), while the latter checks that ↵ = β does not hold, and this includes the case in which any of the two is undefined.

One interesting result is that we can fully capture propositional HT and equilibrium logic in HTC with integer variables and linear constraints. To do so, it suffices to replace each occurrence of a Boolean variable p in a propositional HT theory by the constraint xp = 1 for a corresponding integer variable xp. Then, we get an obvious one-to-one mapping where each assignment (p↪ t) in an HT model corresponds to (xp↪ 1) in HTC and vice versa.

For any linear expression ↵, we define df ↵ def = ↵  ↵ to stand for "↵ is defined," that is, ↵ has a value. It is easy to see that df ↵ is equivalent to the conjunction Vx2Vars(↵) df x. Therefore, if ↵ does not contain integer variables, df ↵ = >.

Constraints in rule heads must be handled with care because they treat all variables, in principle, in a non-directional way. For instance, imagine we want to assign to x some value in the range from0 to y, and that we have the rule y = 10 p but currently no evidence about p so y should be undefined. Adding the formula 0  x ^ x  y would not yield the desired effect because, as we force both constraints to be true, it would also allow for justifying any arbitrary value for y. To allow for directional assignments, we introduce the following construction. An assignment A for variable x is an expression of the form x := ↵ ▷▷ β (with ↵↪ β linear expressions) standing for the formula:

where df A def = df ↵ ^ df β. We say that A is applicable in hH↪ Ti when hH↪ Ti ♣= df A. We define Φ(A) to be the non-directional version of assignment A, that is, Φ(x := ↵ ▷▷ β) def = ↵  x ^ x  β. As we can see, A

3 When we write x = y for two variables, we deal with some syntactic ambiguity wrt '=' used as identity constraint atom. In fact, for integer variables, the semantics of both formulas coincide.

makes some additional checks regarding the definedness of ↵ and β before imposing any condition on x. In particular, (df A ! ↵  x ^ x  β) guarantees that ↵ and β can be used to fix the value of x, but not of variables in ↵ and β themselves. On the other hand, ≻≻df A can be seen as a constraint checking that ↵ and β must be eventually defined in the stable model, but through other rule(s) in the program.

When the upper and lower bounds coincide, we just write (x := ↵) def = (x := ↵ ▷▷ ↵), that is, ≻≻df ↵^(df ↵ ! x = ↵). Note that, as a result, Φ(x := ↵) = (x = ↵).

The following proposition relates A and its non-directional version, Φ(A), in some particular cases.

Proposition 6 Given an assignment A = (x := ↵ ▷▷ β) then:

In particular, if A = (x := ↵ ▷▷ β) contains no variables other than the assigned x, then df A = > and so A ⌘ Φ(A).

We now define an interesting syntactic subclass of HTC logic programs. A linear constraint rule, or LC-rule for short, is a rule of the form:

with n ≥ 0 and k ≥ m ≥ 0, where each Ai is an assignment and each Bj is a linear constraint. For any rule r like (8), we let Head(r) stand for the set of assignments ¶A1↪ ▷ ▷ ▷ ↪An♦ and Body(r) be the set of linear constraints ¶B1↪ ▷ ▷ ▷ ↪Bm↪ ≻Bm+1↪ ▷ ▷ ▷ ↪ ≻Bk♦. An HTC program consisting of LC-rules only is called LC-program.

Notice that an LC-rule does not directly correspond to an HTC program rule since the assignments in the head contain nested implications like (7). However, the following theorem allows us to rewrite any LC-rule as a set of HTC rules, and helps us to illustrate the intuitive behavior of assignments:

Theorem 2 A rule r as in (8) is equivalent 4 to the conjunction V∆✓Head(r) ∆ where ∆ is the implication:

Due to Proposition 6, each implication in Theorem 2 can be written as a set of HTC rules, because Φ(A) is a conjunction in the head ↵  x ^ x  β and, by De Morgan, ≻Φ(A) becomes a disjunction in the body ≻(↵  x)_≻(x  β), and both cases can be unfolded in HT into different rules. Let us informally illustrate this result with the following example.

Example 2 The LC-rule

corresponds to the set of HTC rules:

Suppose our LC-program consists of rule (9) only. The intuition is that ≻(1  z) should hold, as z is undefined and we cannot prove 1  z, but then y := x - 1 cannot be fulfilled, since there are no assignments for x, so it is left undefined and x-1 cannot be evaluated. As a result, we get no stable model. Note how, if we replaced y := x - 1 by just y = x - 1 in the head, we would get a stable model T = ¶(y↪ d)↪ (x↪ d - 1)♦ per each d 2 Z so the rule would also be fixing values for x. Looking at the translation in (10)-(11), the behavior of the assignment becomes clearer. As z does not occur in any head, it is left undefined. Variable x occurs in the head of (10), but it depends on df x in the body, and so, this rule cannot be used to provide a founded value for x. Thus, x is undefined and y = x - 1 is also false, so the constraint (11) becomes applicable, and we get no stable model.

4 A more succinct translation is used in Section 4.

To illustrate non-monotonicity, suppose we add the rule x := 1 whose translation from Theorem 2 amounts to the fact x = 1. Then, we obtain a unique stable model ¶(x↪ 1)↪ (y↪ 0)♦. Moreover, assume now that together with x := 1, we also add the assignment z := 0 ▷▷ 3. This last version of the program yields four stable models: one with z = 0 and y = 0 and the other three with y undefined and z varying from 1 to 3.

The next example illustrates the behavior of an LC-rule with a disjunction in the head.

Example 3 The LC-rule:

corresponds to the conjunction of the HTC-rules:

If we only have (12) in our program, then x and y are undefined and the rule cannot be satisfied - constraint (16) is applicable. If we add, for instance, the assignment x := 1, then y is still undefined, but (14) becomes applicable and we get the stable model ¶(x↪ 1)↪ (z↪ 1)♦. Then, if we further add y := 2, we obtain the two expected stable models ¶(x↪ 1)↪ (y↪ 2)↪ (z↪ 1)♦ and ¶(x↪ 1)↪ (y↪ 2)↪ (t↪ 2)♦. To illustrate how disjunction interacts with positive cycles, let us look at the following variation.

Example 4 Take the program containing (12) and the rules:

If we apply the first disjunct in (12), we get z = 1 and then y = 1 by (18) leading to the stable model ¶(x↪ 1)↪ (y↪ 1)↪ (z↪ 1)♦. This is indeed the only stable model of the program. If we tried to apply the second disjunct in (12) instead, we would need to establish a founded value for y first. However, y depends on z which, in its turn, depends on x through the first disjunct of (12). But then the solution ¶(x↪ 1)↪ (y↪ 1)↪ (z↪ 1)↪ (t↪ 1)♦ would not be minimal. 5

5 As in standard ASP, stable models of a positive HTC program are always minimal wrt set inclusion.

We show next that LC-programs can be translated into ASP with linear constraints, viz. CASP [Gebser et al., 2009], by introducing some auxiliary propositional variables. CASP semantics was based on the assumption that all constraint variables were defined and rigid, that is, the choice axiom x = x is satisfied for any variable x. Let DF stand for the set of choice axioms x = x for all variables in X .

Proposition 7 For any linear expression ↵: DF ♣=df ↵ ⌘ >

Let ⇧ be an LC-program for signature ⌃ = hX↪ Z↪Ai where A is a set of linear constraints. We define a set of auxiliary propositions P = ¶xδ ♣ x 2 X♦. Intuitively, a proposition xδ represents the fact that variable x has a defined value in the original program ⇧. The translation of ⇧ gives a new HTC program ⌧(⇧) for the extended signature ⌧ (⌃) = hX [ P↪ Z [ ¶t♦↪ A [ Pi. For any linear expression ↵, we write ↵δ to stand for the conjunction of all propositions yδ for all y 2 Vars(↵) and (↵  β)δ to stand for the conjunction ↵δ ^ βδ . Using this notation, the translation of a linear constraint A is the formula ⌧(A) def = A ^ Aδ . Intuitively, due to the choice axiom DF (applied only on X), A can hold due to an arbitrary assignment of variable values, but Aδ guarantees that all variables have been assigned a founded value wrt program ⇧. Notice that the translation of df ↵ corresponds to ⌧(df ↵) = ⌧(↵  ↵) = ↵  ↵ ^ ↵δ and, under the assumption DF, the latter is equivalent to ↵δ (Proposition 7). For any arbitrary formula φ, ⌧(φ) stands for the replacement of every constraint atom A in φ by ⌧(A). The translation of an LC-program ⇧ corresponds to the set of formulas ⌧(⇧) def = ¶⌧(r) ♣ r 2 ⇧♦.

As we see below, the models of the translation ⌧(⇧) are isomorphic to the original models of ⇧. Thus, we can apply ⌧ on rules of the form (8) or on their decomposition through Theorem 2. As an example, if we apply the translation on the decomposition of (12) as (13)-(16), we obtain, after some minor simplifications, the rules:

Given a valuation v for the extended signature ⌧(⌃), we define its corresponding "defined" subset in signature ⌃ as v♣δ def = ¶(x↪ d) 2 v ♣ (xδ ↪ t) 2 v♦.

Proposition 8 Given a pair of partial valuations H ✓ T for signature ⌧ (⌃), we have H♣δ ✓ T ♣δ .

Lemma 1 Let hH↪ Ti be an HTC interpretation for signature ⌧(⌃). Then, for any constraint atom A 2 A, hH↪ Ti ♣= ⌧(A) iff hH♣δ↪ T♣δi ♣= A.

By a simple application of structural induction, we get:

Corollary 1 Let hH↪ Ti be an HTC interpretation for signature ⌧(⌃). Then, for any formula ', hH↪ Ti ♣= ⌧(') iff hH♣δ↪ T♣δi ♣= '.

Theorem 3 (Soundness) Let T be a stable model of ⌧(⇧) [ DF . Then, T ♣δ is a stable model of LC-program ⇧.

Theorem 4 (Completeness) Let T be a stable model of LCprogram ⇧. Then, any T 0 such that T 0 ♣=DF and T 0 ♣δ = T is a stable model of ⌧(⇧) [DF .

That is, each stable model T of ⇧ is in one-to-one correspondence to a class of stable models T 0 of ⌧(⇧) [DF that coincide with T in the valuation of its defined variables, making xδ true for all of them, and freely varying the other variables. For instance, the above program ⇧ consisting of (12) plus the facts x := 1 and y := 2 has two stable models T1 = ¶(x↪ 1)↪ (y↪ 2)↪ (z↪ 1)♦ and T2 = ¶(x↪ 1)↪ (y↪ 2)↪ (t↪ 2)♦. Then, ⌧(⇧) includes formulas (20)-(23) plus the translation of the facts, viz. x = 1 ^ xδ and y = 2 ^ yδ . Also, DF includes axioms x = x, y = y and z = z. The resulting translation ⌧(⇧)^DF yields two sets of stable models: one of the form ¶(x↪ 1)↪ (y↪ 2)↪ (z↪ 1)↪ (xδ ↪ t)↪ (yδ ↪ t)↪ (zδ ↪ t)↪ (t↪ d)♦ and another ¶(x↪ 1)↪ (y↪ 2)↪ (t↪ 2)↪ (xδ ↪ t)↪ (yδ ↪ t)↪ (tδ ↪ t)↪ (z↪ d)♦ in both cases for any d 2 D.

4 An LC-solver implementation

We implemented our approach (see [LC2CASP, 2016]) as an extension of the CASP solver CLINGCON 3 [Banbara et al., 2016]. Our system computes the stable models of an LCprogram by implementing a polynomial-size variant of the translation described in the previous section. This is accomplished by using auxiliary atoms to avoid the exponential blow-up in Theorem 2 (similar to [Tseitin, 1968]).

In the input language, rule heads are formed by means of the functor &assign. More precisely, a disjunctive head A1; ▷ ▷ ▷ ;An as in (8) is represented as '&assign { A1;▷ ▷ ▷;An }'. Similarly, linear expressions are formed using the &sum functor. A linear constraint of form '↵1 + · · · + ↵n ≺ β' is written as '&sum { ↵1;▷ ▷ ▷;↵n } ≺ β', where ≺ is among <=, =, >=, <, >, or !=. Moreover, the language contains an all-different constraint, &distinct, as well as a &show and &minimize directive with the same meaning as in ASP yet applied to linear expressions. As with ASP, undefined variables are not shown (eg. t and z above, respectively); also, they do not contribute to minimization.

For illustration, consider the HTC-program in (1) to (4) expressed as an LC -program:

1 n(1..8). 2 :- not &distinct { q(X) : n(X) }. 3 :- &sum { q(X); -q(Y) } = X-Y, n(X), n(Y), X != Y. 4 :- &sum { q(X); -q(Y) } = Y-X, n(X), n(Y), X != Y. 5 &assign { q(1) := 1 } :- not &sum { q(1) } != 1. 6 &assign { q(X) := 1..n } :- n(X), X > 1.

Note that atoms, like n(X) and X > 1, are Boolean propositions, mixed with constraint atoms. The above LCprogram has 4 stable models, all assigning 1 to q(1) according to the default expressed in Line 5. However, once '&assign { q(1) := 4 }.' is added, the default is overwritten, and we obtain 18 models, yet all assigning 4 to q(1).

5 Discussion

We introduced the logic HTC in order to capture constraint theories in the non-monotonic setting known from ASP. As a result, HTC allows for assigning default values to constraint variables or to leave them undefined. To the best of our knowledge, HTC constitutes the first logical account of nonmonotonic constraint theories. Since HT and thus also ASP constitute special cases of HTC, we obtain a uniform framework integrating ASP and CP on the same semantic footing. In view of this, we particularly elaborated on the HTC fragment of LC-programs dealing with linear constraints on integer variables. A central concept is that of assignments (in rule heads) because they are the only way to attribute values to constraint variables - unassigned variables stay undefined.

Our approach is different from traditional CASP [Baselice et al., 2005; Balduccini, 2009; Gebser et al., 2009], where logic programs are hybridized with constraint atoms having standard monotonic CP semantics. In such approaches, constraint atoms in rule heads are merely shortcuts for the complementary body literal. Rather, the monotonic CP semantics assigns each variable all feasible values. In fact, we have identified the HTC fragment corresponding to the approach of [Gebser et al., 2009] and pinpointed the axioms characterizing the aforementioned feature. Although we have not proven it, the result should also extend in a slightly different form to the approaches in [Baselice et al., 2005; Balduccini, 2009] due to their close correspondence to [Gebser et al., 2009] established in [Lierler, 2014]. A noteworthy exception among CASP approaches is Bound Founded ASP [Aziz et al., 2013] that imports the notion of non-circular value derivations into CP. Informally, constraints can have a distinguished variable (akin to a head) over a totally ordered domain. The singular value of a lower-bound 6 variable is the smallest derivable value or the smallest domain element. This yields also a non-monotonic approach that comprises ASP as a special case. However, it remains future work to identify the fragment of HTC that captures this approach and its notion of value minimization.

Our semantics captures a fragment of ASP with partial functions [Cabalar, 2011; Balduccini, 2012] where constraint variables correspond to 0-ary functions. This fragment is expressive enough to cover the general case, since arbitrarily nested partial functions can be reduced to the 0-ary case by a process called flattening [Cabalar, 2011] or unfolding [Bartholomew and Lee, 2013]. Moreover, our approach extends functional ASP by generalizing equality among terms to arbitrary relations. In this paper, we have focused on linear constraints, but other extensions will be studied in the future.

For implementing the fragment of LC-programs, we have devised a translation into CASP programs in accord with [Gebser et al., 2009] and shown its soundness and completeness. The key role in this translation is played by propositions warranting the non-circularity of constraint assignments. Although our system uses CLINGCON as back-end, our translational approach applies also to other CASP solvers sharing the same semantics. Our system along with several examples and additional material is available at [LC2CASP, 2016].

6 And analogously for upper-bound variables.

Acknowledgments This work was partially funded by DFG grant SCHA 550/9.