Declarative Programming of Search Problems with Built-in Arithmetic

1 Introduction

Several lines of work in "constraint modelling languages" or "declarative programming for search problems" aim to produce high-level declarative languages for representing combinatorial search problems, together with solvers for applying these languages in practice. Underlying much of this work is a common logical task of model expansion. Defined for an arbitrary logic L, the task is:

Model Expansion for logic L (abbreviated L MX)

Given: 1. An L-formula φ

2. A structure A for a part σ of vocab(φ)

Find: an expansion B of A that satisfies φ.

We call the vocabulary of A the instance vocabulary, and ε := vocab(φ)\σ the expansion vocabulary. In the combined setting an instance consists of a structure together with a formula. We focus here on the parameterized setting, where a fixed formula for each problem constitutes of a problem specification. An instance is a finite structure, and each expansion of this structure that satisfies the formula is a solution.

Ex. 1 The following formula φ of first order logic constitutes an MX specification for Graph 3-colouring:

An instance is a structure for vocabulary σ = {E}, i.e., a graph A = G = (V ; E). The task is to find an interpretation for the symbols of the expansion vocabulary ε := {R,B,G} such that the expansion of A with these is a model of φ:

The interpretations of ε, for structures B that satisfy φ, are exactly the proper 3-colourings of G.

Systems explicitly based on MX for FO (with extensions), are reported in [Mitchell et al., 2006; Wittocx and Marien, 2008]. It is not hard to see that model expansion underlies many other languages for modelling combinatorial problems, including many not explicitly based on logic (see, e.g., [Mitchell and Ternovska, 2008]).

A benefit of formalization in logic is that descriptive complexity theory, the study of the relationship between computational complexity and expressiveness of logics [Immerman, 1999], provides tools for analyzing and controlling the expressive power of modelling languages. For example, Fagin's theorem [Fagin, 1974], states that the classes of finite structures definable in ∃SO are exactly those in NP. It is equivalent to say that parameterized FO MX captures NP, so FO MX is a natural formal basis for languages to model NP search problems. Capturing results such as Fagin's theorem provide valuable practical, as well as scientific, information. The fact that FO MX can express every problem in NP assures sufficient expressiveness for a user with an NP search problem. That it can express no problem beyond NP provides assurance of reasonable implementability, for example by polytime grounding (automated reduction to, e.g., SAT).

Remark 1 Since FO MX can specify exactly the problems that ∃SO can, one might ask why we use a new term. Primarily it is because we rarely use pure FO MX other than for expository purposes. We employ a variety of logics related to particular goals or particular practical modelling languages. In this paper we restrict FO formulas to those in a certain guarded form, but also extend these with inductive definitions.

Formalizing Arithmetic FO MX can express every problem in NP, but when numerical properties are involved numbers must be encoded with collections of abstract domain elements, and arithmetic operations defined by relations over these encodings. Having "built-in" arithmetic constructs is more natural, and is essential to practical languages.

Arithmetic involves an infinite domain, so limiting the expressive power of a language with arithmetic requires bounding the range of quantified variables and expansion predicates. Imposing such bounds may alter the standard semantics of arithmetic operators, and seems to make expressiveness analysis difficult. Adding built-in numbers can easily produce inadvertent increases in expressive power (see [Mitchell and Ternovska, 2008]). Moreover, when we restrict a language to NP in a direct way, it is not clear if all arithmetic properties in NP can be expressed using the built-in arithmetic. For example, a common method to is to represent numbers with tuples of domain elements. However, this approach provides a much smaller fragment of arithmetic, and a much weaker theorem, than we obtain here.

Almost all declarative languages for modelling combinatorial problems have some form of bounded-domain arithmetic. In many cases, this arithmetic has not been formalized. To our knowledge, capturing of NP with built-in arithmetic has not been shown in any area of declarative programming. Arithmetic in has been formalized in related settings, such as database query languages, but no work we are aware of addresses the concerns of this paper.

This report takes steps toward a logical foundation for constraint modelling languages with built-in arithmetic, and methods for controlling their expressive power. We believe the way we do this formalizes much that is done in practice, but without formalization, in some existing languages. Ultimately, we want to produce practical, fully formalized, languages in which modellers may use built-in arithmetic in the most natural way possible. Further, we want to precisely control the expressive power of these languages, in particular to express exactly the NP search problems, with minimal restrictions on syntax.

Contributions We develop a notion of embedded model expansion with an infinite background structure, in particular for arithmetic structures which include the usual functions on the natural numbers (or integers), as well as aggregates such as those used in SQL and many constraint languages (Sec. 2); We introduce a logic for producing embedded MX specifications, which is a variant of the k-guarded fragment of FO (or FO(ID)), in which upper and lower guards control access to the infinite background domain (Sec. 2); We show that, on classes of "small-cost" structures, where numbers are not allowed to be too large, this logic captures NP (Sec. 3); We generalize this result to an extension of classical logic with inductive definitions to allow poly-size "user-defined" guards (Sec. 4).

2 EmbeddedMXwith Arithmetic

Embedded finite model theory (see [Libkin, 2004]), the study of finite structures whose domain is drawn from some infinite structure, was introduced to study databases that contain numbers and numerical constraints. Rather than think of a database as a finite structure, we take it to be a set of finite relations over an infinite domain.

Def. 1 A structure A is embedded in an infinite background (or secondary) structureM= (U; ¯M) if it is a structure A = (U ; ¯R) with a finite set ¯R of finite relations and functions, where ¯M ∩ ¯R = ∅. The set of elements of U that occur in some relation or function of A is the active domain of A, denoted adomA.

In database research, embedded structures are used with logics for expressing queries. Here, we use them in logics for MX specifications (which are second order queries). The vocabularies for these logics consist of 1) σ, the vocabulary of A, which is our instance structure; 2) ν, the vocabulary of an infinite secondary structure M = (U; ¯M), such as the arithmetical structure defined below; and 3) ε, an expansion vocabulary. A formula φ over σ ∪ ν ∪ ε constitutes an MX specification. The model expansion task remains the same: expand an embedded σ-structure to satisfy φ.

To limit the expressive power of logics for MX with infinite secondary structures, we must limit the range of quantified variables and the range of expansion predicates. For this, we use an adaptation of the guarded fragment GFk of FO [Gottlob et al., 2001]. In formulas of GFk, a conjunction of up to k atoms acts as a guard for each quantified variable.

Def. 2 The k-guarded fragment GFk of FO is the smallest set of formulas that: 1) contains all atomic formulas; 2) is closed under Boolean operations; 3) contains ∃ ¯x(G1∧. . .∧Gm∧φ), provided the Gi are atomic formulas, m ≤ k, φ ∈ GFk, and each free variable of φ appears in some Gi.

Here, G1 ∧ . . . ∧Gm is called the guard of ¯x. Since GFk is closed under negation, universal quantification can be treated as an abbreviation in the usual way, so universal quantifiers are guarded as in ∀¯x(G1 ∧ . . . ∧ Gm ⊃ φ).

To limit the range of domain elements that may occur in expansion predicates, we introduce GGFk, a restriction of GFk where we require and axiom limiting the range of each expansion predicate.

Def. 3 The double-guarded fragment GGFk(ε) of FO, for a given vocabulary ε, is the set of formulas of the form φ ∧ ψ, with ε ⊂ vocab(φ ∧ ψ), where φ is a formula of GFk, and ψ is a conjunction of guard axioms, one for each symbol of ε occurring in ψ, of the form

where m ≤ k, and the union of free variables in the Gi is precisely ¯x.

For expansion functions, the guard axiom is on the graph of the function, i.e., ∀¯x∀y (f(¯x) = y ⊃ φ(¯x, y)), where φ is a conjunction of atoms.

We call the guards of GFk, which restrict the range of quantified variables, lower guards, and the guard axioms of GGFk(ε) upper guards. Initially, we require all atoms providing upper and lower guards to be from the instance vocabulary, so ranges of variables and expansion predicates are explicitly limited to adomA. We later relax this restriction, adding a mechanism for "user-defined" guard relations that may contain elements not in adomA. For convenience only, we assume that the instance vocabulary always contains the predicate symbol adom. Then adom(x) can be used as a guard (upper or lower).

Upper and lower guards provide a logical formalization of the type systems of some existing constraint modelling languages [Mitchell and Ternovska, 2008]. Lower guards correspond to declaring the types of variables, and upper guards to declaring the types of arguments to expansion predicates.

Remark 2 FO MX corresponds to ∃SO, and similarly GGFk(ε) MX corresponds to k-guarded ∃SO, where all variables, first order and second order, have guards.

For writing MX specifications for embedded structures, we extend the logic GGFk(ε) with vocabulary for a fixed background structure M. We will talk about "GGFk(ε) MX specifications with background structure M".

The background structure of interest here is the arithmetical structure which we now describe. (This structure is the same as that used in [Gr¨adel and Gurevich, 1998].) In addition to standard arithmetical operators, it has a collection of multiset operations, including max, min, sum and product. For any set R, fm(R) denotes the class of all finite multisets over R. Any function f : U → U defines a multiset mult(f) = {{f(a) : a ∈ U}} over U, the domain of A. A multiset operation (or aggregate) is a function Γ : fm(U) → U.

Def. 4 An Arithmetical structure is a structure N containing at least (N; 0, 1, χ,<,+, ·,min,max, ∑, ∏), with domain N, the natural numbers, and where min, max, ∑, and ∏ are multi-set operations and χ[φ](¯x) is the characteristic function. Other functions, predicates, and multi-set operations may be included, provided every function and relation of N is polytime computable.

Our logic for GGFk(ε) MX specifications with background structure N is obtained by extending GGFk(ε) with terms constructed from the vocabulary of N , which we now define. As usual, φ(¯x) denotes that ¯x contains the free variables of φ.

Def. 5 (well-formed terms) Let τ be the vocabulary σ∪ν∪ε and V a countable set of variables. The set of well-formed terms is the closure of the sets of variables V and constants of τ under the following operations:

1. If f is a τ-function of arity n, other than a multiset operation or the characteristic function, and ¯ t is a tuple of terms of length n then f(¯ t) is a term.
2. If Γ is a multiset operation of ν, f(¯x, ¯ y) a term, and φ(¯x, ¯ y) a τ-formula in which ¯x is guarded, then Γ¯x(f(¯x, ¯ y) : φ(¯x, ¯ y)), is a term with free variables ¯ y.
3. If φ(¯x) is a τ-formula such that ∃ ¯xφ(¯x) is a k-guarded formula, then χ[φ] is a term with free variables ¯x.

Multiset operations (case 2) act much like quantifiers, binding the variables ¯x. Notice that the free variables ¯ y in φ, within a multiset operation term, need not be guarded within φ. Their guards are in the formula where the term appears.

Semantics of multiset terms Let G(¯ y) be the multiset term Γ¯x(f(¯x, ¯ y) : φ(¯x, ¯ y)). The interpretation of G(¯ y) on τstructure D with valuation ¯b for ¯ y is

As usual, A |= φ[¯a] means that formula φ(¯x), is true in structure A when the free variables ¯x denote domain elements ¯a.

The index ¯x in the term Γ¯x is not needed in the semantic definition (1) - think e.g. of Γ being summation (Σ). For readability, we may omit φ when true and write Γ¯x(f(¯x, ¯ y)); omit free variables and write Γ¯x(f : φ).

The interpretation of the characteristic function χ[φ](¯x) on τ -structure D with valuation ¯a for ¯x is: χ[φ]D (¯a) = 1 if D |= φ[¯a] and 0 otherwise. We may write Γ¯x(f × χ[φ]) instead of Γ¯x(f : φ) when Γ is invariant under multiple occurrences of 0 in the multiset (i.e., Γ(S) = Γ(S ∪ {{0, . . . , 0}})), as is the case for Σ and max on N .

Def. 6 An embedded GGFk(ε) MX specification with secondary structure N is a set of GGFk(ε) sentences over σ ∪ ε ∪ ν, with terms as in Definition 5, and the secondary ν-structure is the arithmetical structure of Definition 4.

In our presentation here, all elements of the active domain are drawn from the arithmetical background structure. All results of the paper generalize to the multi-sorted case, including the case where some domains are not ordered.

Remark 3 One may imagine it would be easier to use a more restricted arithmetic structure, say without multiset functions. In fact, for our main result (Theorem 1), all the difficulty is present as soon as we have numbers and addition. Moreover, the multiset operations make proving the theorem easier.

We now give examples of embedded MX specifications with secondary structure N, for search versions of two common optimization problems.

Ex. 2 KNAPSACK: Instance vocabulary {O,w, v, bv, bw}, where O is the set of objects; w is the weight function; v is the value function; bw is the weight bound; and bv is the value bound. Expansion vocabulary {O′ }, where O′ is the set of selected objects. Upper guard axiom: ∀x(O′ (x) ⊃ O(x)). Axioms are Σx(w(x) : O(x) ∧O′ (x)) ≤ b and k ≤ Σx(v(x) : O(x) ∧O′ (x)), where t1 ≤ t2 is an abbreviation for t1 < t2 ∨ t1 = t2. The lower guard for O(x) ∧O′ (x) is O(x). ✸

Ex. 3 MACHINE SCHEDULING PROBLEM [Hooker, 2000]: We must assign jobs to machines to satisfy constraints on release and due dates and a cost bound. The instance lists jobs, machines, possible start times, the release date and due date for each job, the cost and duration for running each job on each machine, and the cost bound. The instance vocabulary, σ, consists of: Job(j), the set of jobs to be scheduled; Machine(m), the set of machines to perform jobs; Time(t), all possible starting times; ReleaseDate(j), a release date for each job; DueDate(j), a due date for each job; Cost(j,m), cost of doing job j on machine m;

Duration(j,m), the duration of executing j on m; and c, the cost bound. The active domain consists of all time points, costs, due and release dates, durations, jobs and machines. The expansion vocabulary consists of two functions: Assignment(j) maps jobs to machines and StartTime(j) maps jobs to start times.

Upper guard axioms:

∀j∀m (Assignment(j) = m ⊃ Machine(m) ∧ Job(j)) ∀j∀t (StartT ime(j) = t ⊃ T ime(t) ∧ Job(j))

Axioms:

Σj(Cost(j,Assignment(j)) : Job(j)) ≤ c ∀j(Job(j) ⊃ StartT ime(j) ≥ ReleaseDate(j)) ∀j(Job(j) ⊃ StartT ime(j)+Duration(j)≤DueDate(j)) ∀t (T ime(t) ⊃ (∀m (Machine(m) ⊃ maxj (countj (ψ(j, m, t))) = 1)).

In the last axiom, which specifies that at most one job is on a machine at a time, countj(ψ(j,m, t)) is an abbreviation for Σj(χ[ψ(j, m, t)]), and ψ defines the set of jobs being executed on machine m at time t, that is, ψ(j,m, t) is:

Job(j) ∧ Assignment(j) = m ∧ T ime(StartT ime(j))

∧ StartT ime(j) ≤ t ∧ t < StartT ime(j) + Duration(j, Assignment(j)),

It is easy to see that all axioms are in GGFk(ε). ✸

An optimization version would include the objective function: minimizing: Σj(Cost(j,Assignment(j)) : Job(j)).

SQL Examples The following SQL query returns the maximum value in column k among the tuples in table T that satisfy the Boolean condition C: SELECT MAX(k) FROM T WHERE C. It is represented by the multiset operation: maxxk {{xk : ∃x1 . . . ∃xk-1∃xk+1 . . . ∃xnT(¯x) ∧ C(¯x)}}, where ¯x := x1 . . . xn. The following query returns the number of rows in T that satisfy the Boolean condition C: SELECT COUNT(*) FROM T WHERE C. Its representation is: Σ¯x(χ[T(¯x) ∧ C(¯x)]). We have expressed all other SQL aggregates, but for brevity omit them here.

3 Capturing NP in the Presence of Arithmetic

Here, we present our main result. It can be applied to any language which is a syntactic variant of our language, for example a suitable fragment of ESSENCE. We consider the decision problem associated with embedded MX, in the parameterized setting (data complexity), where the formula is fixed and instances are finite structures.

The size of an embedded structure A is the size of its active domain, i.e., |A| = |adomA|. We define the cost of A to be cost(A) = ⌈log(l)⌉, where l is the largest number in adomA. A class K of embedded arithmetical structures has small cost if there is some k ∈ N such that cost(A) < |A|k , for every A ∈ K. This is a generalization of the notion of a metafinite structure with small weights of [Gr¨adel and Gurevich, 1998]. The cost of A is the size of the binary encoding of its largest number, so small cost structures have encodings that are of size polynomial in their domain size. Small cost structures have no numbers larger than 2poly(|A|) .

A class K of τ -structures is an embedded spectrum if there is a first-order sentence φ of a vocabulary τ ′ := τ ∪ε of logic GGFk(ε) such that D ∈ K iff there exists an expansion D′ of D with D′ |= φ.

Theorem 1 Let K be an isomorphism-closed class of smallcost arithmetical embedded structures over vocabulary σ. Then the following are equivalent: (1) K ∈ NP, (2) K is an embedded spectrum.

The proof of Theorem 1 essentially reduces this statement to Fagin's theorem, by considering a class of related structures in which numbers are encoded by relations over (abstract) domain elements. For this, we need enough domain elements to encode the largest number, and this is where the small-cost restriction comes from. We believe it is possible to obtain a similar result under a weaker restriction.

4 User-Defined Guard Relations

So far, the numbers that may occur in a solution for an instance are restricted to those that occur in the instance (that is, adomA), because expansion predicates have upper guards composed only of instance predicates. There are many problems where this is too restrictive, an obvious example being integer factorization. (We can define many search problems with "new" numbers in solutions, but these numbers must be encoded with elements of the instance structure, rather than appearing directly.) To relax this limitation, we introduce "user-defined guard relations". We now consider specifications consisting of two formulas, D and φ. Formula D is over vocabulary σ ∪ δ, where δ is a set of predicate symbols not in σ, and for each instance structure A, D defines an expansion of A′ that includes the new user-defined guard relations. The active domain of A′ will be the union of adomA and any elements of the defined guard relations. Formula φ of GGFk(ε), over vocabulary σ ∪ δ ∪ ν ∪ ε, defines an embedded model expansion task for each A′ . That is, φ is such a specification with a larger instance vocabulary σ ∪ δ.

Informally, D should be a device for defining sets of numbers beyond those in the instance, in the aid of letting φ be a more natural axiomatization of the problem than it could be without these extra guard relations. For D to fullfill this role, the relations it defines should be unique (for each instance), and easy to compute. Formally, we require D satisfy the following property.

Property 1 (Good D) We call D good if it defines a total function fD from embedded σ-structures to embedded σ ∪ δstructures and is fD is polytime computable.

We may choose to use a syntax for D that is distinct from that of φ. Whatever the syntactic form we choose for D, we will require that it is in some logic with the property that, for every allowed D, it is decidable (preferably in polytime) if D is good (satisfies property 1). Thus, we can effectively decide if a specification has appropriate user-defined guard relations.

Capturing NP with User-Defined Guards

Let us denote by DGGFk(ε, δ) a logic obtained by an extension of GGFk(ε) to allow specification of user-defined guards as just described. A DGGFk(ε, δ) MX specification φ ∧ D with background structure N is defined as in Definition 6, except that it also includes the part D.

Lemma 1 Let φ∧D be a DGGFk(ε, δ) MX specification with N , where D is good. Let K be a small cost class of embedded σ-structures, and K′ be the class of σ ∪ δ-structures obtained from K by expanding each structure of K with the relations defined by D. That is, K′ = {fD(A) : A ∈ K}. Then the following are equivalent: (1) K is in NP (2) K′ is in NP, (3) K is an embedded spectrum, (4) K′ is an embedded spectrum,

AGood D for N. Lemma 1 gives general conditions under which we may capture NP with user defined guard relations. In general, similar conditions will hold for many choices of secondary structure, and for each there will be many choices for the form of D that will satisfy those conditions. We now present one choice for the form of D that satisfies the conditions in the case of arithmetical structures. We wish to choose this form so that easily checkable syntactic conditions are sufficient to ensure a given D is good.

Our guard relations will be defined by induction, using the syntax and semantics of FO(ID), the extension of FO with inductive definitions (see [Denecker and Ternovska, 2008]). Inductive definitions are specified with a rule-based syntax, with arbitrary FO formulas in the bodies, under the 2-valued well-founded semantics. We give an example, and refer to [Denecker and Ternovska, 2008] for details of syntax and semantics. The odd numbers on N: {∀x (Odd(x) ← x = 0 ∨ ∃y (Odd(y) ∧ x = y + 2))} The defined (intensional) symbols are those in the head, and open (extensional) are the rest. We assume that definitions contain no free variables, and every variable that occurs in the head also appears in the body. Each definition may simultaneously define several relations.

Def. 7 Say a formula ψ of FO(ID) is in form DEF if:

1. ψ is a conjunction of definitions of FO(ID) having a well-founded partial pre-order on definitions such that all open (extensional) symbols are either from σ (the instance vocabulary) or defined by a definition which is strictly smaller in the pre-order. (We may also combine all definitions into one large stratifiable definition.)
2. Each definition is either: (a) Of the form {∀ x (G(x) ← x ≤ size(φ))}, where size(φ) is Σx(χ[adom(x))), or (b) either positive or stratifiable, and every rule is of the form { ∀¯x ¯ y (G(¯x, ¯ y) ← y1 = t1(¯x) ∧ . . . ∧ yk = tk(¯x) ∧ φ(¯x) }, where k ≥ 0 and ∃ ¯x φ(¯x) is guarded, and guards are either from the input structure, or are defined earlier in the pre-order.

Lemma 2 It is polytime decidable if a formula is in the form DEF. If D is in formDEF, it is good.

Theorem 2 DGGFk MX with background structures and D in form DEF captures NP on small cost structures.

Ex. 4 Suppose we have a search problem on weighted directed graphs, and are interested only in nodes within some particular distance of a given node s. In our MX axiomatization, we may need a guard P(x) which represents this set of nodes. We have a sequence of definitions (Δ1,Δ2,Δ3):

where adom is the active domain of the instance. The guard defined in Δ1 restricts allowable distances.

which defines the distances to all nodes reachable from s provided they are within the distance bound.

which defines the set of all nodes within the pre-specified distance from the node s.

Adding Inductive Definitions to DGGFk

In [Mitchell and Ternovska, 2005; Mitchell et al., 2006], we proposed to use FO(ID), rather than just FO, as the basic logic for MX specificying NP search problems. Here, again, we find FO(ID) convenient 1 . A generalization of GFk to the case with inductive definitions is given in [Patterson et al., 2007]. The logics used in the present paper also may be extended with inductive definitions, and the main results will still hold.

5 RelatedWork

In database theory, embedded model theory (see [Libkin, 2004]) and metafinite model theory [Gr¨adel and Gurevich, 1998; Gr¨adel, 2007], both extend finite model theory to handle applications with infinite domains. Our development closely follows that of [Gr¨adel and Gurevich, 1998], although we use the embedded setting and the guarded logic defined above.

Embedded Model Theory We have taken the embedded models approach in our work, so some results in the area may be useful, but none so far addresses our immediate needs, such as giving conditions for capturing a complexity class. Much work in the area reduces questions about queries over embedded finite models to questions about normal finite models. Many of these results are restricted to generic queries, but declarative programming axiomatizations are rarely generic. An important result is the natural-domain-active-domain collapse for ∃SO for finite models embedded in an infinite structureM. This holds if SO quantification is over subsets of the active domain only, but this is too restrictive for us, because solutions to search problems often involves numbers not contained in the instance.

Metafinite Structures [Gr¨adel and Gurevich, 1998] are sorted structures D = (A,R,W), where A is a finite primary structure, R is the secondary structure, and W is a set of "weight functions" from Ak to R. Typically, R is a fixed infinite structure, such as the arithmetic structure N that we also use.

1 Formally we can do without inductive definitions, since FO MX has the same power as ∃SO. However, expressing transitive closure and many other useful concepts is impractically complex in ∃SO.

Logics for Metafinite Structures are designed to allow application of methods of finite model theory. These are twosorted logics, interpreted over combined two-sorted structures. In [Gr¨adel and Gurevich, 1998], the logics contain, in addition to the standard terms, weight terms which denote functions from the primary to the secondary part. New weight terms can be built by applying functions of the secondary structure to applications of other weight terms.

To obtain capturing of NP, the authors of [Gr¨adel and Gurevich, 1998] define a notion of metafinite spectrum, a counterpart to the generalized spectra in Fagin's sense, and restrict attention to metafinite spectra of structures with "small weights" i.e., if w is a weight function, and w(¯a) = s then |s| = poly(|A|). Our "small cost" structures and embedded spectra are generalizations of these concepts.

The work of Gr¨adel and Gurevich to a large degree inspired our work here. However, their requirement of "no quantification over the secondary structure" was too restrictive for our purposes. In [Gr¨adel and Gurevich, 1998], access to the secondary structures is through weight terms only. In natural MX specifications, quantification over elements of background structures is essential. Instead of weight terms of [Gr¨adel and Gurevich, 1998], we allow arbitrary mixed relations, and introduced guarded quantification. Using lower guards was not sufficient - on arithmetical structures, unrestricted metafinite spectra capture the r.e. sets [Gr¨adel and Gurevich, 1998], which would imply the same property for our formalism. Thus, we needed upper guards as well. In our proof of capturing NP, we needed to develop a way to deal with numbers appearing as arguments of expansion predicates, which was not needed in [Gr¨adel and Gurevich, 1998].

Other Related Work The authors of [Cadoli and Mancini, 2006] expressed the view that ∃SO is a good mathematical abstraction of practical constraint languages in which to carry out a general study of techniques for reasoning about specifications. They explain that ∃SO is expressive enough to axiomatize finite arithmetic (e.g. modulo domain size), i.e., guess tables for e.g. addition, and reject those not satisfying axioms for addition. Our goal was to formalize built-in arithmetic as in most constraint languages. The MX-based IDP system [Wittocx and Marien, 2008] has a language with arithmetic and aggregates, but we are not aware of a formalization of the arithmetic or expressiveness analysis for the language. LPARSE can express NEXP-complete problems. A version of ASP with infinite domains is described in [Heymans et al., 2006]. The authors study satisfiability problem, not model expansion, and decidability and complexity results for that problem are obtained for several variants of ASP (loosely guarded programs and generalized programs similar to Datalog LITE). We do not see a clear correspondence between the guarded logics we use here and the loosely guarded fragment used in [Heymans et al., 2006]. No work we are aware of has presented a framework for search problems with built-in arithmetic where the user is given an assurance of universality for a given complexity class.

Acknowledgments

We are grateful to Brendan Guild, Toni Mancini and anonymous referees for discussions and comments.