Grounding for Model Expansion in k-Guarded Formulas with Inductive Definitions

1 Introduction

NP search and decision problems occur widely in AI; modelling these problems as SAT, CSP and ASP and then using a corresponding solver are perhaps the most successful declarative approaches (in practice) to solving these problems. While each approach has made valuable contributions, they also have limitations. Modelling in propositional logic and then using a SAT solver is the oldest and the most developed of these approaches; the simplicity of the semantics has been the key driver in its success. However, propositional logic provides a poor modelling language in which there are no quantifiers, nor recursion. Moreover, in modelling a problem as SAT, there is no clear separation of instance and problem description. CSP provides somewhat better modelling capabilities, and CSP solvers rely on a number of solution techniques such as no-good learning and backjumping. CSP solvers, however, have found success primarily as components of general purpose programming languages, and are thus not purely declarative. ASP emerged from logic programming, and is based on the stable model semantics [Gelfond and Lifschitz, 1991]. The main advantage of ASP is that its language allows an implicit use of quantifiers and has a built-in recursion mechanism. However, some concepts that are natural in classical logic are difficult to express in ASP.

Mitchell and Ternovska [2005] proposed a declarative constraint programming framework based on classical logic extended with inductive definitions. They cast search problems as the classical problem of model expansion (MX), which is the problem of expanding a given structure with new relations so that it satisfies a given formula. Their long-term goal is to develop tools for solving hard combinatorial search problems, especially those in NP. In this framework, a problem is encoded in a logic such as first-order logic (FO) or an extension of FO, a problem instance is represented by a finite structure, and a solver generates extensions of initially unspecified predicates, which represent solutions to the problem.

The MX framework combines many strengths of these three mentioned approaches, as well as addresses their limitations. Its features include: a high-level modelling language that supports quantification and recursion, and a clear separation of the instance (a finite structure) from the problem description (a formula). Most importantly, the framework is based on classical logic, making it possible to exploit the many existing results from finite model theory and descriptive complexity [Kolokolova et al., 2006]. In addition, axiomatizations are easier to understand, and we need not rely on stable model semantics to imitate the 'classical' part of the program, a common practice in ASP.

A key component in building practical solvers for the MX framework is propositionalisation (or grounding) of highlevel specifications and the use of efficient SAT solvers. The idea is to first obtain a ground formula that contains only initially unspecified predicates and is satisfiable iff the original MX problem has a solution, and then call a propositional satisfiability solver. Two prototype solvers for propositional formulas with inductive definitions have been developed [Pelov and Ternovska, 2005; Mari¨en et al., 2005].

The goal of this paper is to develop an efficient grounding algorithm for the MX framework. Since the framework is based on classical logic, we take advantage of results known for the guarded fragments [Andr´eka et al., 1998;

Gottlob et al., 2001]. We present a polytime algorithm for grounding k-guarded FO sentences with inductive definitions provided that all predicates in the guards are initially specified (a fragment which we call IGFk). As explained later, this restriction is necessary for polytime grounding, and IGFk contains (in terms of expressive power) sentences with treewidth at most k. In practice, most sentences have small treewidth and thus can be put into IGFk with small k. Our algorithm runs in O(ℓ2nk ) time, where ℓ is the size of the sentence, and n is the size of the structure.

2 Grounding for Model Expansion (MX)

We formulate search problems as the problem of model expansion (MX).

Definition 2.1 (MX) Given a sentence φ and a finite structure A with vocabulary σ ⊆ vocab(φ), find a structure B that is an expansion of A to vocab(φ) such that B |= φ.

Example: Let A be a graph G = (V ; E), and let φ be:

Let B be an expansion of A to vocab(φ). Then B |= φ iff it corresponds to a 3-coloring of G.

In the MX framework, there is a clear separation between problem instance (finite structure) and problem description (a formula). In grounding, we bring domain elements into the syntax by expanding the vocabulary and associating a new constant symbol with each element of the domain. For domain A, we denote the set of such constants by ˜ A. As notational conventions, we use σ to denote the instance vocabulary and ε the expansion vocabulary.

Definition 2.2 (Reduced Grounding for MX) A formula ψ is a reduced grounding of a formula φ over a σ-structure A = (A, σA) if (1) ψ is a ground formula over ε ∪ ˜ A; and (2) for every expansion structure B = (A, σA , εB ) over vocab(φ), B |= φ iff (B, ˜ AB) |= ψ, where ˜ AB denotes the interpretation of the new constants ˜ A.

During grounding, the symbols of the instance vocabulary are "evaluated out" and a reduced grounding is obtained.

Obviously, by the above definition, we have

Proposition 2.3 Let ψ be a reduced grounding of a formula φ over a σ-structure A. Then A can be expanded to a model of φ iff ψ is satisfiable.

Thus, through grounding, the model expansion problem is reduced to the satisfiability problem.

In our grounding algorithm for a sentence, we must deal with subformulas φ of the original sentence (φ may contain free variables). For a σ-structure A, we compute a formula ψ for each instantiation of the free variables of φ, such that each ψ is a reduced grounding of φ under the corresponding instantiation. We call such a representation an answer to φ wrt A. We compute an answer to a formula, by computing answers to its subformulas and combining them according to the connectives. To represent such answers, we introduce the concept of an extended relation (extending the notion of a relation from relational database theory).

Definition 2.4 (extendedX-relation) Let A = (A; σA), and X be the set of free variables of formula φ. An extended X-relation R over A is a set of pairs (γ, ψ) s.t. (1) ψ is a ground formula over ε ∪ ˜ A and γ : X → A; (2) for every γ, there is at most one ψ s.t. (γ, ψ) ∈ R.

An extended X-relation R is intended to represent a unique mapping (denoted by δR) from all possible instantiations of variables in X to ground formulas. For γ's not appearing in R, the associated formula is false. We write γ ∈ R to mean that there exists ψ such that (γ, ψ) ∈ R.

Definition 2.5 (answer to φ wrt A) Let φ be a formula in σ ∪ ε with free variables X, A a σ-structure with domain A, and R an extended X-relation over A. We say R is an answer to φ wrt A if for any γ : X → A, we have that δR(γ) is a reduced grounding of φ[γ] over A. Here, φ[γ] denotes the result of instantiating free variables in φ according to γ.

As an example, let φ = ∃x∃y∃zφ′ where φ′ = P (x, y, z)∧ E(x, y) ∧ E(y, z), σ = {P}, and ε = {E}. Let A be a σ-structure such that P A = {(1, 2, 3), (3, 4, 5)}. Then this extended relation R

is an answer to φ′ wrt A. It is easy to see, for example, that δR(1, 2, 3) = E(1, 2) ∧ E(2, 3) is a reduced grounding of φ′ [(1, 2, 3)] = P(1, 2, 3) ∧ E(1, 2) ∧ E(2, 3), and δR(1, 1, 1) = false is a reduced grounding of φ′ [(1, 1, 1)]. The following extended relation is an answer to φ′′ = ∃zφ′

Here, for example, E(1, 2) ∧ E(2, 3) is a reduced grounding of φ′′ [(1, 2)]. Finally, the following represents an answer to φ, where the single formula is a reduced grounding of φ.

Just as relations in databases have an algebra, i.e., a set of operations whose semantics correspond to the connectives of FO logic, we define an algebra for extended relations. Our algebra consists of join, join with complement, projection, intersection and union.

Definition 2.6 (join, join with complement) Let R be an extended X-relation and S an extended Y -relation, both over domain A. Then

1. the join of R and S is the extended X ∪ Y -relation R✶ S = {(γ, ψ) | γ : X ∪ Y →A, γ|X ∈ R, γ|Y ∈ S, and ψ = δR(γ|X) ∧ δS(γ|Y )};
2. the join of R with the complement of S is the extended X ∪ Y -relation R ✶c S = {(γ, ψ) | γ : X ∪ Y → A, γ|X ∈ R, and ψ = δR(γ|X) ∧ ¬δS(γ|Y )}.

Proposition 2.7 Suppose that R is an answer to φ1 and S is an answer to φ2, both wrt structure A. Then (1) R ✶ S is an answer to φ1 ∧ φ2 wrt A; (2) R ✶c S is an answer to φ1 ∧ ¬φ2 wrt A.

Definition 2.8 (Y -projection) Let R be an extended Xrelation and Y ⊆ X. The Y -projection of R, denoted by πY (R), is the extended Y -relation {(γ ′ , ψ) | γ ′ = γ|Y for some γ ∈ R and ψ = ∨{γ∈R|γ|Y =γ ′ } δR(γ)}.

Proposition 2.9 Suppose that R is an answer to φ wrt A, and Y is the set of free variables of ∃¯ zφ. Then πY (R) is an answer to ∃¯ zφ wrt A.

Definition 2.10 (intersection, union) Let R and S be extended X-relations. Then

1. the intersection of R and S is the extended X-relation R ∩ S = {(γ, ψ) | γ ∈ R and γ ∈ S, and ψ = δR(γ) ∧ δS (γ)};
2. the union ofRandS is the extendedX-relationR∪S = {(γ, ψ) | γ ∈ R or γ ∈ S, and ψ = δR(γ) ∨ δS(γ)}.

Proposition 2.11 Let φ1 and φ2 be formulas with the same set of free variables. Suppose that R is an answer to φ1 and S is an answer to φ2, both wrt A. Then (1) R∩ S is an answer to φ1 ∧ φ2 wrt A; (2) R ∪ S is an answer to φ1 ∨ φ2 wrt A.

In traditional relational algebra, projection can be done in linear time, and join can be done in time linear in the sum of the size of the input and output relations. Detailed algorithms and proofs for this can be found in the appendix of [Flum et al., 2002]. The essential idea is this: first encode domain elements appearing in the input relations by natural numbers; then sort the encoded input relations using the bucket sort algorithm; next, compute the projection or join of the encoded input relations; finally, decode the resulting output relation. In our implementation of the operations on extended relations, we use the same idea except that we also need to copy formulas from the input relations to the output relation.

Let R be an extended X-relation. The size of R, denoted by ‖R‖, is the sum of the size of each pair (γ, δR(γ)) in R. Thus ‖R‖ = |X||R| + ∑γ∈R ‖δR(γ)‖, where |R| denotes the cardinality of R as a set, and ‖δR(γ)‖ is the size of the formula associated with γ. It is easy to see that projection takes O(‖R‖) time, and intersection and union take time O(‖R‖ + ‖S‖). In general, join and join with complement take time O(‖R‖ · ‖S‖). However, in our grounding algorithm in the next section, whenever we perform an R ✶ S or R ✶c S operation, it is always the case that the set of variables of S is a subset of that of R, every formula in R is true, and every formula in S is of size O(ℓ), where ℓ is the size of the formula to be grounded. So the relation part (the set of tuples) of the resulting extended relation is a subset of that of R. Thus both operations can be done in time O(ℓn), where n is the size of the relation part of R.

3 An Algorithm for Grounding FO Formulas

The guarded fragment GF of FO was introduced by Andr´eka et al. [1998]. Here, any quantified subformula φ must be relativized by a guard, i.e., an atomic formula over all free variables of φ. Gottlob et al. [2001] extended GF to the k-guarded fragment GFk where the conjunction of up to k atoms may act as a guard, and proved that k-guarded sentences can be evaluated in time O(ℓ2nk ) where ℓ is the size of the formula, and n is the size of the structure. The proof is by transforming GFk-sentences into k-guarded Non-Recursive Stratified Datalog (NRSD) programs.

A fragment related to GFk is the bounded variable fragment of FO - FOk , which denotes FO formulas that use at most k distinct variables. Kolaitis and Vardi [1998] showed that conjunctive queries in FOk have the same expressive power as conjunctive queries of treewidth at most k. Gottlob et al. [2001] obtained a similar logical characterization for the notion of hypertreewidth, a generalization of treewidth. They noted that hypertreewidth is bounded above by treewidth and showed that GFk has the same expressive power as FO sentences of hypertreewidth at most k.

Definition 3.1 (GFk) The k-guarded fragment GFk of FO is the smallest set of formulas s.t. (1) GFk contains atomic formulas; (2) GFk is closed under Boolean operations; (3) GFk contains ∃¯x(G1 ∧ . . . ∧Gm ∧φ), if the Gi are atomic formulas, m ≤ k, φ ∈ GFk, and the free variables of φ appear in the Gi. Here G1 ∧ . . . ∧ Gm is called the guard of φ.

Note that this definition also includes universal quantification, since by (2), GFk is closed under negation. Also note that the above mentioned complexity result O(ℓ2nk ) only applies to k-guarded sentences, not k-guarded formulas in general. To see why, by the definition, ¬R(x, y, z) is a 1-guarded formula, but it cannot be evaluated in O(n) time. However, the same complexity result applies to strictly k-guarded formulas, defined as follows:

Definition 3.2 (SGFk) The strictly k-guarded fragment SGFk is the fragment of GFk with formulas of the form ∃¯x(G1 ∧ . . . ∧ Gm ∧ φ).

Here, we are including the degenerate cases where ¯x is empty (no leading existential quantifier), m = 0 (no free variables and therefore no guards), or φ is true. Thus any k-guarded sentence is strictly k-guarded (take ¯x as empty and m = 0).

Liu and Levesque [2003] presented a polytime algorithm for evaluating strictly k-guarded formulas: Given a structure A and a formula φ ∈ SGFk, the algorithm computes the answer to φ wrt A, that is, {γ | A |= φ[γ]}, in time O(ℓnk ). A reason that they considered strictly k-guarded formulas instead of just k-guarded sentences is that their algorithm is recursively defined. In this section, we adapt their algorithm for grounding formulas in the following fragment:

Definition 3.3 (RGFk) RGFk denotes the set of strictly kguarded formulas such that no expansion predicate appears in any guard.

Note that the restriction that "no expansion predicate appears in any guard" is necessary for polytime grounding. Indeed, there is no polytime grounding algorithm for 1-guarded sentences; otherwise, we would have a polytime reduction to SAT from MX for 1-guarded sentences, and hence the combined complexity of this problem would be in NP. However, it is NEXP-complete since MX for FO can be reduced to MX for 1-guarded sentences [Kolokolova et al., 2006], and the combined complexity of MX for FO is NEXP-complete.

It is easy to see that any FOk formula can be rewritten in linear time into an equivalent one in RGFk, by using atoms of the form x = x as parts of the guards when necessary. For example, the formula ∃x∃y[R(x) ∧E(x, y)] can be rewritten into ∃x∃y[R(x) ∧ y = y ∧ E(x, y)], where R is an instance predicate, and E is an expansion predicate. Extending the result of [Kolaitis and Vardi, 1998], Flum et al. [2002] showed that FOk has the same expressive power as FO formulas of treewidth at most k. Thus any FO formula with treewidth at most k can be put into an equivalent one in RGFk. In practice, most formulas have small treewidth and thus can be put into RGFk with small k.

Our grounding algorithm uses extended relations and operations on them. If φ is an atomic formula R(¯ t ), we use φ(A) to denote the extended relation {(γ, true) | ¯ t [γ] ∈ RA}.

Procedure Gnd(A, φ)

Input: A structure A and a formula φ ∈ RGFk

Output: An answer to φ wrt A

Suppose φ(¯x) = ∃¯ y(G1 ∧ . . . ∧ Gm ∧ ψ). Return π¯xGnd(A,R, ψ′ ), where R is G1(A) ✶ . . . ✶ Gm(A), and ψ′ is the result of pushing ¬'s in ψ inward so that they are in front of atoms or existentials.

Procedure Gnd(A, R, φ) is defined recursively by:

1. If φ is a positive literal of an instance predicate, then Gnd(A, R, φ) = R ✶ φ(A);
2. If φ is ¬φ′ , where φ′ is an atom of an instance predicate, then Gnd(A, R, φ) = R ✶c φ′ (A);
3. If φ is a literal of an expansion predicate, then Gnd(A, R, φ) = {(γ, φ[γ]) | γ ∈ R};
4. Gnd(A,R, (φ ∧ψ)) = Gnd(A,R, φ) ∩Gnd(A,R, ψ);
5. Gnd(A,R, (φ ∨ψ)) = Gnd(A,R, φ) ∪Gnd(A,R, ψ);
6. Gnd(A,R, ∃¯ yφ) = R ✶ Gnd(A, ∃¯ yφ);
7. Gnd(A,R, ¬∃¯ yφ) = R ✶c Gnd(A, ∃¯ yφ).

Unfortunately, the running time of Gnd is not O(ℓnk ) anymore. The reason is that Gnd may generate intermediate extended relations whose size is not O(nk ). To see why, let φ be the 1-guarded formula ∃x[R(x) ∧ ∃y(S(y) ∧ E(y))], where E is an expansion predicate, and let A be a structure such that RA = {2i + 1 | 0 ≤ i ≤ m}, and SA = {2i | 0 ≤ i ≤ m}. Obviously, the formula ∨mi=0 E(2i) is a reduced grounding of φ over A, and it has size O(n). However, when we use Gnd, the intermediate extended relation corresponding to the subformula R(x) ∧ ∃y(S(y) ∧ E(y)) has size O(n2 ), as shown in the following table (on the left):

To solve this problem, we let IGnd be the algorithm which is the same as Gnd except for the following: After each projection operation, we replace each formula in the resulting extended relation by a new propositional symbol. We also save the definitions of these new symbols. The output of the algorithm is the final extended relation together with the definitions of all the new symbols. For instance, in the above example, we will introduce a new propositional symbol p and save the definition p ≡ ∨mi=0 E(2i). Then the intermediate extended relation corresponding to the subformula R(x) ∧ ∃y(S(y) ∧ E(y)) will be as in the table on the right, and it has size O(n).

To illustrate the algorithm, let φ be the formula

where T and E are expansion predicates, and let A be

RA = {(1, 2, 1), (1, 2, 2), (7, 0, 2), (7, 0, 3)},

SA = {(2, 2, 5), (2, 3, 9), (4, 0, 2), (6, 7, 8)},

AA = {(1, 2, 6), (7, 0, 2), (7, 0, 5)}, BA = {(2, 3, 4), (3, 7, 5)},

CA = {(1, 2), (2, 2), (5, 2), (6, 2), (6, 3), (9, 6)},

Then φ ∈ RGF2, where the underlined parts are guards. First, we push negation symbols inward until they are in front of atoms or existentials. The following figure represents the resulting formula by a tree, where rectangular internal nodes stand for guarded existentials, circular internal nodes for disjunctions or conjunctions, and leaves for literals.

p1 ≡

p2 ≡

p3 ≡

E(2,

4)

E(0,

4)

true

Now that we have an answer to this bottom existential, we process the top existential in a similar way for the final answer

Proof Sketch: Rewrite φ into an equivalent formula φ′ by pushing negations inwards. Correctness then follows by induction on the formula according to the algebra for extended relations. As to complexity, for each intermediate extended relation, there are O(nk ) tuples (each guard is composed of at most k atoms), and each formula has size O(ℓ), due to the introduction of new propositional symbols. By the complexity analysis from Section 2, each of the O(ℓ) operations on extended relations can be done in time O(ℓnk ).

4 Grounding Inductive Definitions

While FO MX is often sufficient, modelling often requires recursion and recursion through negation. The solution is to use FO(ID) logic, which is FO extended with inductive definitions [Denecker, 2000; Denecker and Ternovska, 2004]. Fortunately, adding inductive definitions does not violate the main complexity-theoretic results [Mitchell and Ternovska, 2005; Kolokolova et al., 2006].

The syntax of FO(ID) is that of FO extended with a rule saying that an inductive definition (ID) is a formula. An ID Δ is a set of rules of the form ∀¯x(X(¯ t) ← φ), where X is a predicate symbol, ¯ t is a tuple of terms, and φ is an arbitrary FO formula. The connective ← is called the definitional implication. In the rule ∀¯x(X(¯ t) ← φ), X(¯ t) is called the head and φ the body. A defined predicate of an FO(ID) formula is a predicate symbol that occurs in the head of a rule in an ID. The semantics of FO(ID) is that of FO extended with one additional rule saying that a structure A satisfies an ID Δ if it is the 2-valued well-founded model of Δ, as defined in the context of logic programming [van Gelder et al., 1993].

For example, the problem of finding the transitive closure of a graph can be conveniently represented as an MX problem for FO(ID). The formula consists of a definition with two rules, defining the predicate T . The instance vocabulary has a single predicate E, representing the binary edge relation.

This states that the transitive closure of edge set E is the least relation containing all edges and closed under reachability.

When it comes to MX for FO(ID), the expansion vocabulary usually includes all the defined predicates. All the definitions from Section 2, namely definitions of MX, reduced grounding, extended relation, and answer, directly apply to FO(ID). Also, through grounding, the MX problem for FO(ID) is reduced to the satisfiability problem of PC(ID), which stands for propositional calculus with inductive definitions. Currently, two prototypes of such solvers have been developed: one [Pelov and Ternovska, 2005] reduces satisfiability of PC(ID) to SAT, and the other [Mari¨en et al., 2005] is a direct implementation that incorporates SAT techniques. While, both solvers deal with a restricted PC(ID) syntax, a solver for the general syntax is under construction in our lab.

Nonetheless, some important problems are represented as MX for FO(ID) where some defined predicates are in the instance vocabulary. The interpretation of these defined predicates is used to apply restrictions on the possible interpretations of the expansion predicates. In such a case, we will first do grounding treating all defined predicates as expansion predicates. Let ψ be the resulting ground formula. Then we add to ψ an extra constraint that encodes the interpretation of the defined predicates. Suppose G is the set of ground atoms of interpreted defined predicates that appear in ψ. Let ϕ be the conjunction of literals of G that are true according to the interpretation. Then ψ ∧ ϕ is the final ground formula to be passed to the satisfiability solver. Thus we can restrict our attention to grounding where all defined predicates are expansion predicates.

In this section, we extend the algorithm from Section 3 to ground FO(ID) formulas in the following fragment:

Definition 4.1 (IGFk) IGFk is the extension of RGFk with inductive definitions such that for each rule, the body is in RGFk and all free variables of the body appear in the head.

As with RGFk, any FO(ID) formula with at most k distinct variables can be rewritten in linear time into an equivalent one in IGFk. Here we show how to rewrite each rule so that it satisfies the restriction of the above definition. First, for each x that appears in the head but not the body, add x = x to the body. Now since the body still uses at most k distinct variables, it can be rewritten into RGFk.

We first present a procedure for grounding IDs:

Procedure GndID(A, Δ)

Input: A structure A and an ID Δ ∈ IGFk

Output: An answer to Δ wrt A

For each rule r of Δ, suppose r is ∀¯x(X(¯ t) ← φ), let Δr be {X(¯ t)[γ] ← ψ | (γ, ψ) ∈ IGnd(A, φ)}. Return ⋃r∈Δ Δr.

To illustrate the procedure, let Δ be the ID

where T is an expansion predicate. Then Δ ∈ IGF2. Note that for the purpose of illustration, we use C(y) instead of y = y as a part of the second guard so that we can produce a small grounding. Let A be EA = {(1, 2), (2, 3)}, and CA = {(3)}. GndID(A,Δ) would proceed as follows:

1. Call IGnd(A,E(x, y)) to get R
2. Call IGnd(A, ∃z(C(y) ∧ E(x, z) ∧ T (z, y))) to get S
3. Replace rule 1 with {T (x, y)[γ] ← ψ | (γ, ψ) ∈ R}
4. Replace rule 2 with {T (x, y)[γ] ← ψ | (γ, ψ) ∈ S} The resulting ground ID is

We now extend the grounding algorithm IGnd from Section 3 by adding the following clause. We call this enhanced algorithm for grounding IGFk formulas IGnd+.

1. If φ is an ID Δ or its negation ¬Δ, then IGnd(A,R, φ) = {(γ, p) | γ ∈ R} or {(γ, ¬p) | γ ∈ R}, where p is a new propositional symbol with the definition p ≡ GndID(A, Δ).

The following is the main theorem of this paper:

Theorem 4.2 Given a structure A and a formula φ ∈ IGFk, IGnd+ returns an answer to φ wrt A in O(ℓ2nk ) time, where ℓ is the size of φ and n is the size of A.

5 RelatedWork

Our grounding algorithm is inspired by the grounding part of the model-checking algorithm of Datalog LITE [Gottlob et al., 2002], which is essentially 1-guarded Datalog and admits model checking in time linear in both the size of the structure and the size of the formula. However, our grounding is aimed for the more general problem of model expansion. Our algorithm also has similarity with the grounding techniques of the ASP systems Smodels [Syrj¨anen and Niemel¨a, 2001], Cmodels-2 [Lierler and Maratea, 2004], and DLV [Leone et al., 2006], and the constraint programming system NP-SPEC [Cadoli and Schaerf, 2001]. These systems produce efficient groundings in practice, however, they use logic programming syntax, which is much more restrictive. The precise complexity of grounding for these systems has not been determined, while we give an apriori time bound. Finally, Ramachandran and Amir [2005] proposed polytime algorithms to propositionalise certain classes of FO theories so that satisfiability is maintained. Their goal is to solve satisfiability problem, not MX.

6 Conclusions

Classical logic is perhaps the most natural language for axiomatizing and solving computational problems. It has a long history, and sophisticated techniques have been developed. Classical logic has intuitive and well-understood semantics, convenient syntax, and it is widely used by both theoreticians and practitioners. We therefore believe that tools based on classical logic to the highest degree possible will have a strong appeal. The MX framework of Mitchell and Ternovska [2005] is a constraint programming framework based on classical logic extended with inductive definitions. This paper represents an important progress in making this framework practical by developing an efficient grounding algorithm. The algorithm performs well on k-guarded FO sentences with inductive definitions under the restriction that all predicates in the guards are initially specified; it runs in time O(ℓ2nk ), where ℓ is the size of the formula, and n is the size of the structure. To this end, we have proposed the concept of extended relations and defined an algebra on them. The essence of our work is to exploit the structure of FO formulas: Indeed, k-guarded formulas have the same expressive power as formulas with hypertreewidth at most k. A grounder based on the data structure of extended relations has been implemented in our group. It performs comparably on similar inputs to systems mentioned in related work.