Computer Science
Computer Science-2021.gz:143485
Computer Science
37c2624492440d3fb81ab35fd7a132dc87d6dead
FOLASP: FO(.) as Input Language for Answer Ser Solvers

Over the past decades, Answer Set Programming (ASP) has emerged as an important paradigm for declarative problem solving. Technological progress in this area has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in non-monotonic reasoning, efforts have also been made to reconcile ASP with classical first-order logic (FO). This has resulted in the development of FO(.), an expressive extension of FO, which allows ASP-like problem solving in a purely classical setting. This language may be more accessible to domain experts already familiar with FO, and may be easier to combine with other formalisms that are based on classical logic. It is supported by the IDP inference system, which has successfully competed in a number of ASP competitions. Here, however, technological progress has been hampered by the limited number of systems that are available for FO(.). In this paper, we aim to address this gap by means of a translation tool that transforms an FO(.) specification into ASP-Core-2, thereby allowing ASP-Core-2 solvers to be used as solvers for FO(.) as well. We present experimental results to show that the resulting combination of our translation with an off-the-shelf ASP solver is competitive with the IDP system as a way of solving problems formulated in FO(.). Under consideration for acceptance in TPLP.


Introduction
Answer set programming (ASP) is a knowledge representation (KR) paradigm in which a declarative language is used to model and solve combinatorial (optimization) problems (Marek and Truszczyński 1999). It is supported by performant solvers , such as Clingo ) and the DLV system (Leone et al. 2006). Development and use of these solvers has been simplified and encouraged by the emergence of the unified ASP-Core-2 standard (Calimeri et al. 2020).
The roots of ASP lie in the area of non-monotonic reasoning and its semantics is defined in a non-classical way. Work by Denecker et al. (Denecker and Ternovska 2008) has attempted to integrate key ideas from ASP with classical first-order logic (FO), in an effort to clarify ASP's contributions from a knowledge representation perspective. This has resulted in the development of the language FO(·), pronounced "ef-oh-dot", which is a conservative extension of FO. This language may be easier to use for domain experts who are already familiar with FO than ASP, and can seamlessly be combined with other monotonic logics. A number of systems, such as the IDP system (De Cat et al. 2016) and Enfragmo (Aavani 2014), already support the FO(·) language. However, when compared to the variety of solvers for ASP-Core-2, the support arXiv:2108.04020v1 [cs.AI] 9 Aug 2021 for FO(·) is still rather limited. This hinders technological progress, both in terms of solver development and the development of applications.
In this paper we present FOLASP, a tool that translates FO(·) to ASP-Core-2, thereby allowing each solver that supports ASP-Core-2 to handle FO(·) as well. In this way, we significantly extend the range of solvers that is available for FO(·).
We believe that this tool will make the FO(·) language more accessible and useful for practical applications, while also helping to drive technological progress. To develop FOLASP, we build on fundamental results about the relation between ASP and FO(·) (Mariën et al. 2004;Denecker et al. 2012), which we have for the first time combined into a working tool.

FO(·)
FO(·) is an extension of classical typed first-order logic with aggregates, arithmetic, and (inductive) definitions. To maximize clarity, we will consider only a core subset of FO(·): typed FO extended with definitions, cardinality aggregates, and comparison operators.
A structure S for a vocabulary V (also known as a V -structure) consists of a domain D and an appropriate interpretation σ S for each symbol σ ∈ V . The interpretation T S of a type T is a subset of D, the interpretation P S of a predicate P with τ (P ) = (T1, . . . , Tn) is a relation P S ∈ T S 1 × · · · × T S n , and the interpretation F S of a function symbol F with τ (F ) = (T1, . . . , Tn, Tn+1) is a function from T S 1 × · · · × T S n to T S n+1 . The interpretations T S i of the types Ti ∈ V partition the domain D, i.e., i T S i = D and T S i ∩ T S j = ∅ for i = j. A term is either a variable, an integer, a function f ( t) applied to a tuple of terms t, or a cardinality expression of the form #{ x : ϕ( x)}, which intuitively represents the number of x's for which ϕ( x) holds. Note that cardinality expressions are a special case of a aggregate expressions, which sometimes are introduced as generalized quantifiers working as atoms. Here, we use the FO terminology, where a cardinality expression is a term.
We use the notion of a simple term to refer to a variable or an integer. An atom is either a predicate P ( t) applied to a tuple of terms or a comparison t1 t2 between two terms, with ∈ {=, =, ≤, ≥, <, >}. As usual, formulas are constructed by means of the standard FO connectives ¬, ∨, ∧, ⇒, ⇔, ∃, ∀. Only well-typed formulas are allowed. A sentence is a formula without free variables. A positive literal is an atom, a negative literal a negated atom.
where P/n is a predicate symbol, x1, . . . , xn variables, and ϕ a formula. The atom P (x1, . . . , xn) is the head of the rule, while ϕ is the body. The purpose of such a definition is to define the predicates that appear in the heads of the rules in terms of the predicates that appear only in the body. The first kind of predicates are called the defined predicates Def (∆) of the definition ∆, while the second are called its open predicates Open(∆).
The formal semantics of these definitions is given by a parametrized variant of the wellfounded semantics (Van Gelder et al. 1988). In order for a definition to be valid in FO(·), it must be such that it uniquely determines a single interpretation for the defined predicates, given any interpretation for the open predicates. Formally, the condition is imposed on definitions that their well-founded model must exist and always be two-valued, no matter what the interpretation for their open predicates might be.
Different logical inference tasks can be considered for FO(·). In this paper, we focus on the most common task, namely that of model expansion.
Definition 1. Let Th be a theory over vocabulary V and S a structure for a subvocabulary V oc(S) ⊆ V . The model expansion problem M X(V, S, Th) is the problem of computing a Vstructure S ⊇ S such that S |= Th.
Example 1. The following example models the well-known graph coloring problem as a model expansion problem M X(V, S, Th), with an illustration of a definition for the symmetric closure of the border relation.

ASP
A normal logic program is a set of rules of the form: H :-B1, . . . , Bm, not Bm+1, . . . , not Bn. (1) Here, H and all Bi are atoms. Corresponding with definitions, H is called the head of the rule, while the conjunction B1, . . . , not Bn is called the body. Both the rule head and body can be empty. A rule with empty head (= false) is called a constraint, a rule with empty body (= true) a fact. The semantics of a program is defined in terms of its grounding which is an equivalent program without any variables, so all atoms are ground atoms. An interpretation I is a set of ground atoms. A rule of form (1) is satisfied in I if H ∈ I whenever B1, . . . , Bm ∈ I and Bm+1, . . . , Bn ∈ I. An interpretation is a model of a program if it is a model of each rule. The reduct of a program P w.r.t. interpretation I, denoted P I , contains the ground rule H :-B1, . . . , Bm for each rule of form (1) for which none of the atoms Bm+1, . . . , Bn belong to I. An interpretation I is a stable model or answer set of program P if it is a minimal model of P I .
The ASP-Core-2 language extends this basic formalism in a number of ways. For instance, it includes choice rules that can be used to express that a certain atom H may be true: {H} :-B1, . . . , Bm, not Bm+1, . . . , not Bn.
Choice rules allow to generate a search space of candidate answer sets, from which the desired solutions can be filtered out with constraints.
A second extension is the cardinality aggregate, which, as in FO(·), counts the size of the set of free variable instantiations for which a conjunction of atoms holds. Throughout this paper, we make use of cardinality aggregates in body atoms, which have the form: #count{ X : B1, . . . , Bm, not Bm+1, . . . , not Bn} t with ∈ {=, =, ≤, ≥, <, >} and t a simple term.
Example 2. The following ASP program is the counterpart of the FO(·) graph coloring model expansion problem from the previous section: country(be). country(nl). country(lux).

Translation of FO(·) to ASP
In this section, we define a translation α from an FO(·) model expansion problem M = M X(V, S, Th) to an ASP program α(M ). The translation α consists of four components α1, α2, α3 and α4. α1 and α2 translate V and S, respectively (discussed in Section 3.2). α3 and α4 translate the FO(·) sentences and definitions that belong to Th, respectively (Section 3.3 and 3.4). Prior to translation we normalize the specification in order to make it compatible for translation to ASP (Section 3.1).

Normalization of an FO(·) specification
As a first step, we normalize the specification of the model expansion problem M X(V, S, Th). Firstly, we convert all formulas in Th to negation normal form (NNF) (Enderton 2001), i.e., the Boolean operators are restricted to negation (¬), conjunction (∧) and disjunction (∨), and the negation operator is only applied directly to atoms. We also assume that the type T of any variable x is known, either by automated type derivation or by an explicit annotation, e.g., ∀x[T ] : ϕ.
In FO(·), a function symbol can be interpreted by any function of the appropriate arity and type. By contrast, in ASP, each function symbol F is interpreted by the Herbrand function that maps each tuple of arguments t to the syntactic term F ( t). Hence, we eliminate function symbols from the FO(·) specification. For this, we first rewrite the theory such that function symbols only appear in atoms of the form F ( x) = y with x and y simple terms. This is done by recursively replacing a (negated) atom (¬)A with subterm F ( t) by the NNF equivalent of In a similar way, we unnest cardinality terms, such that these only occur in a comparison atom with simple terms, i.e., #{ x : ϕ( x)} y with y a simple term. After this, each term t that is not simple occurs only in equality atoms t = x (if t is a function symbol application) or comparison atoms t x (if t is a cardinality expression), with x a simple term.
If the structure S has an interpretation F S , then we replace it by . . , an+1) | (a1, . . . , an) → an+1 ∈ F S }. Finally, after eliminating function symbols, we push negations through atoms of the form t x by adjusting the operator. After this, the only negated atoms remaining have the form ¬P ( x) for some predicate P and simple terms x.
Example 3. The normalized FO(·) graph coloring theory from Section 2.1 is:

Generating the search space
The solutions to a model expansion problem M X(V, S, Th) are to be found among the set of all structures for V that expand S -the search space. In this section, we translate vocabulary V and structure S to generate precisely this search space.
Unlike FO(·), ASP-Core-2 imposes strict naming conventions: variable names must start with a capital, while the names of all other kinds of symbols must start with a lower case letter. For an FO(·) type, predicate, variable or domain element σ, we denote byσ a corresponding ASP symbol of the right kind. Naturally, we enforce thatσ =σ whenever σ = σ .
In a model expansion problem M = M X(V, S, Th), some of the symbols in V are interpreted by S (we denote these by V oc(S)), while others (i.e., V \ V oc(S)) are not. Because types must always be interpreted by S and our normalization step transforms all function symbols into predicates, the uninterpreted vocabulary V \ V oc(S) consists entirely of predicates.
We translate each P ∈ V \ V oc(S) with associated typing τ (P ) = (T1, . . . , Tn) into the following ASP choice rule α1(P ): We translate an interpretation P S = {(a 1 1 , . . . , a 1 n ), . . . , (a m 1 , . . . , a m n )} of an n-ary predicate P into the following set α2(P S ) of m ASP facts: . The interpretation of a type is translated as though it were a unary predicate. The second component α2(M X(V, S, Th)) of our translation now consists of all α2(P S ) for which P ∈ V oc(S). Together, α1 and α2 allow us to generate the correct search space in ASP, as the following theorem shows.
Here, the equality between structures and answer sets is of course modulo a straightforward "syntactic" transformation: we can transform each structure S to the answer set f (S) that consists of all atoms P ( d) for which d ∈ P S . Because we consider a typed logic, in which each element of the domain of S must belong to the interpretation T S of at least one type T , this transformation is an isomorphism, which we omit from our notation for simplicity.
Proof. The set M X(V, S, {}) consists of all V -structures S that can be constructed by starting from the structure S and then adding, for each predicate P ∈ V \ V oc(S) with type τ (P ) = (T1, . . . , Tn), any set of tuples ⊆ T S 1 ×· · ·×T S n as interpretation P S of P in S . For each predicate P interpreted by S, α2(S) contains precisely all facts P ( d) for which d ∈ P S . Moreover, P does not appear in α1(V \ V oc(S)). This ensures that each answer set in AnswerSets(A) contains precisely all atoms P ( d) for which d ∈ P S . For each predicate P ∈ V \ V oc(S), S may have any set of tuples ⊆ T S 1 × · · · × T S n in its interpretation. The choice rules in α2(S) ensure that precisely these tuples also make up the possible interpretations for P in AnswerSets(A).

Translating formulas
We now define a third component α3(M X(V, S, Th)) of our translation to transform the formulas ϕ ∈ Th to ASP. We start by the base case: the translation α3(A) for an atom A. Due to our normalization step, the only atoms A that appear in Th are of the form P ( x) (with P/n a predicate and x a tuple of simple terms) or t x (with t a simple term or a cardinality expression, a comparison operator, and x a simple term). The translation α3(P (x1, . . . , xn)) of a predicate atom is the ASP conjunctioṅ P (ẋ1, . . . ,ẋn),Ṫ1(ẋ1), . . . ,Ṫn(ẋn) with typing τ (P ) = (T1, . . . , Tn). Hence, the type information implicit in the typing of a predicate is added explicitly by means of the additional conjunctsṪi(Xi). With slight abuse of notation, we shorten such a conjunction of type atoms toṪ (˙ x). With x and y simple terms, the translation α3(x y) is the ASP conjunctioṅ The translation α3(#{ x[ T ] : ϕ( x, y)} z) of a normalized cardinality atom is with δ a fresh auxiliary predicate representing the subformula ϕ. Hence, we also add the rule: with a recursive application of α3. After normalization, a negation occurs only in literals of the form ¬P ( x), whose translation α3(¬P ( x)) simply is Note that the not is only added to the first atom and not to the type atoms.
Having defined how each (negated) atom (¬)A is translated into a corresponding ASP expression α3((¬)A), we now inductively define how more complex formulas are translated.
The translation α3(ϕ ∧ ψ) of a conjunction is the ASP conjunction α3(ϕ), α3(ψ). The translation α3(ϕ( x) ∨ ψ( y)) of a disjunction is the ASP atom δ(˙ x,˙ y), with δ a fresh auxiliary predicate. Additionally, for each such auxiliary predicate, we add the following ASP rules: to ensure that δ indeed corresponds to the disjunction of ϕ and ψ.
Since a variable that appears in the body of an ASP rule but not in its head is implicitly existentially quantified, the translation α3(∃x[T ] : ϕ(x)) of an existential quantification is the ASP conjunction α3(ϕ(x)),Ṫ (ẋ).
The translation α3(∀x[T ] : ϕ(x)) of a universally quantified formula is the ASP cardinality atom α3(#{x[T ] : ϕ(x)}) = n, with n = |T S | the number of elements in type T . Note that, because of this step, the translation α3 not only depends on the theory Th of our model expansion problem, but also on the structure S. A first way to avoid this dependence is to translate ∀x[T ] : ϕ(x) as α3(#{x[T ] : ¬ϕ(x)}) = 0. However, this would introduce an additional negation, which might lead to the introduction of loops over negation in Section 3.4. A second way introduces an aggregate term representing n, e.g., α3(#{x[T ] : ϕ(x)} = #{x[T ] : true}), but we expect this to be less efficient.
For any formula ϕ( x), we can now use the transformation α3 to define a fresh ASP symbol δϕ(˙ x) such that the set of all x for which ϕ(x) holds in the FO(·) theory Th coincides with the set of all˙ x for which δϕ(˙ x) holds in the ASP program. We do this by adding the following reification rule rϕ: Theorem 2. Let ϕ be a formula in vocabulary V and let S be a structure for V . Consider the ASP program Rϕ that consists of all reification rules r ψ for which ψ is a subformula of ϕ, together with all additional rules produced by the translation α3 (see Eq. 10 and Eq. 12). Let RS = α2(S) be the translation of the structure S. Then RS ∪ Rϕ has a unique answer set A and for each subformula ψ the set of all d for which S |= ψ( d) is equal to the set of all d for which Proof. RS is a set of facts over V . Rϕ is a strictly stratified set of rules with non-empty heads. Therefore, it is clear that the answer set of RS ∪ Rϕ is indeed unique. We now prove the theorem by induction over the subformula order. The base cases are atoms as translated in Eq. 7 and Eq. 8. Here, it is obvious from the translation that the correspondence holds. For an aggregate (Eq. 10), we can apply the induction hypothesis to obtain a correspondence between the tuples for which ϕ in the original aggregate holds and the tuples for which the fresh predicate δ in its translation holds; from this, the result follows. Similarly, the case for disjunction follows from applying the induction hypothesis to the fresh predicates in Eq. 12. The cases for negation, conjunction and existential quantification are trivial. The case for universal quantification follows immediately from the correctness of the translation of aggregates.
Once we have the reification rules rϕ as defined above, we can eliminate answer sets in which the formula ϕ is not satisfied by adding a constraint :-not δϕ. Denoting such a constraint by Cϕ, the third component of our translation -the translation of sentences -now is where the rules rϕ and constraints Cϕ are as above and R are all of the additional rules (see Eq. 10 and Eq. 12) generated by producing the rϕ. Proof. By induction on the size of Th. The base case in which |Th| = 0 and therefore Th = {} is covered by Theorem 1. Once the induction hypothesis gives us the correspondence between a theory Th of size n − 1 and an ASP program An−1, we can add an additional formula ϕn and prove the correspondence between Th ∪ {ϕn} and An = An−1 ∪ {rϕ n , Cϕ n } ∪ R, with R the additional rules for producing α3(ϕn). The atoms in the head of the new rules {rϕ n , Cϕ n } ∪ R are all fresh atoms that do not appear in An−1. Therefore there can be no interference between the new rules and the old ones, and the result follows from Theorem 2.
We now have a translation for theories that consists entirely of FO sentences. The next section examines how we can extend this to FO(·) theories that contain also definitions.

Translating definitions
In general, a theory in FO(·) can contain multiple definitions. However, it is well-known that each such theory can be transformed into a theory that contains just a single definition (Van Gelder et al. 1991). This involves merging the different definitions and possibly renaming predicates to avoid the introduction of new loops. The necessity for this renaming step can be seen by comparing the following two theories: Th consists of two separate definitions (one defining p in terms of q and the other defining q in terms of p) and Th , which consists of a single definition that jointly defines both p and q: The theory Th has two models, namely {} and {p, q}, while Th has {} as its unique model. We therefore cannot simply merge the two definitions in Th. The solution is to rename the predicates that are defined in (at least one of) these definitions, and then assert the equivalence between the old and the new predicates. More formally, for each definition ∆, for each defined predicate P in ∆, we replace all occurrences of P in ∆ with a fresh unique predicate P∆ and add the equivalence constraint P ⇔ P∆. Applying this merge procedure to Th yields the following theory: This avoids the introduction of additional loops and ensures Th equivalent to the original Th.
We now first show the correctness of this transformation in isolation, before combining it with previous results. Proof. A valid definition in FO(·) must be such that its well-founded model is always two-valued. Because the transformation from ∆ to α4(∆) introduces no additional loops over negation (in fact, it introduces no additional negations at all), the set of ASP rules α4(∆) also has a twovalued well-founded model. It is well known that a two-valued well-founded model is also the unique stable model. Given this uniqueness result, the theorem now follows from the correctness of α3 (Theorem 2).
Note that this theorem does not hold for structures S that interpret some of the defined symbols of ∆. Consider, for instance, the definition consisting only of the rule p ← true and the structure S in which p S = f alse. The problem M X(V, S, ∆) has no solutions, but α2(S) = {} and α4(∆) = {p :-}, which means that α2(S) ∪ α4(∆) has {p} as an answer set.
For the same reason, we cannot simply combine α4(∆) with the choice rules introduced by α1. To solve this problem, we will use the same renaming trick that we use to merge separate definitions.
Definition 2. Let M X(V, S, Th) be a model expansion problem in which the theory Th contains only a single definition ∆, and let Th = Th \ {∆}. Let ∆ be the result of replacing each defined predicate P of ∆ by a fresh predicate P∆, and denote by Eq the set of all equivalence constraints ∀ x : P ( x) ⇔ P∆( x) for defined predicates P . We define α(M X(V, S, Th)) as the following ASP program: α1(M X(V, S, ·)) ∪ α2(M X(V, S, ·)) ∪ α3(M X(·, S, Th ∪ Eq)) ∪ α4(M X(·, S, ∆ )). Proof. Theorem 2 already shows that all parts of the model expansion problem apart from the definition are correctly translated by α1, α2 and α3. Theorem 4 shows that the definition ∆ can be correctly translated by α4(∆). The renaming of the defined predicates of ∆ ensures that both can be combined without invalidating the correctness of either theorem.

Translating the graph coloring example
We now show how M X(V, S, Th ), with Th the normalized theory from Example 3, can be translated to ASP. This translation consists of four parts -α1, α2, α3, α4 -which correspond to the translation of the vocabulary V , the structure S, the constraints in Th , and the definitions in Th , respectively. :-symBorder (C1, C2), not symBorder ∆ (C1, C2).
Example 4 and Example 2 are both ASP programs representing the same graph coloring problem. α1(M ) in Example 4 corresponds to rules (3) and (4) in Example 2, α2(M ) is the same set of facts (2), α3(M ) corresponds to the constraint (5), and α4(M ) corresponds to the rules (6).
It is clear that the translation in Example 4 is a lot less succinct. Firstly, the translation introduces a significant number of auxiliary predicates, both reification predicates δi and a renaming predicate symBorder∆ for the defined predicate of the definition. Secondly, the universal quantifications in the FO(·) specification lead to several cardinality aggregates not present in the original formulation. Thirdly, the FO(·) implication that represents the graph coloring constraint is normalized into a nested disjunction (see Example 3) and this leads to four translated rules, compared to the single rule (5) in Example 2.

Implementation
By implementing this translation, we created a new model expansion engine for FO(·), called FOLASP. It uses the syntax of the IDP system for its input and output, and uses Clingo (Gebser et al. 2019) as back-end ASP solver.
In addition to the subset of FO(·) discussed in this paper, FOLASP also supports minimum and maximum aggregates, arithmetic, function symbols in the head of a definition, partial interpretations, and partial functions. We thereby cover almost all language constructs supported by IDP, except for symbol overloading, chained (in)equalities and constructed types. Besides the model expansion inference, FOLASP also supports the optimization inference, which computes a model that minimizes the value of some integer objective function.
Where appropriate, FOLASP uses the FO(·) type information to add "guards" of the form type(X) for each variable X to the bodies of the generated ASP rules. In other words, FOLASP generates so-called safe rules, which allows the resulting programs to be handled by ASP solvers such as Clingo.
FOLASP is implemented in Python 3. Its source code is published on Gitlab. 1 We tested the correctness of the implementation by checking that the solutions produced by FOLASP are accepted as such by IDP, and that, for optimization problems, the optimal objective values produced by IDP and FOLASP were in agreement.

Experiments
In our experiments, we evaluate FOLASP (commit 82ec7edc on the development branch) using Clingo (version 5.4.0) as backend ASP solver. This configuration is compared to two other approaches. The first comparison approach runs IDP (commit 4be3c797) on the same FO(·) specifications as taken as input by FOLASP. The second comparison runs Clingo (again version 5.4.0) on native ASP encodings of the same problems.
As benchmark set, we use the problem instances from the model-and-solve track of the fourth ASP competition (Alviano et al. 2013). Both IDP and Clingo participated in this competition, which means that we have-for these same problems-both FO(·) and ASP specifications already available, written by experts in both languages. As such, we believe these benchmarks provide a good opportunity for a fair comparison.
We used the scripts and FO(·) specifications from the IDP submission to generate FO(·) instances that are accepted by both IDP and FOLASP. For the ASP system Clingo, we used the native ASP encodings provided by the organizers of the fifth ASP competition (Calimeri et al. 2016) (which uses the same problem set) since Clingo could not parse the specifications from the fourth ASP competition.
IDP solves problems in NP. This covers all problems in the benchmark set, apart from the strategic companies problem, which has a higher complexity. In the competition itself, the IDP team therefore solved this problem using a separate script to generate an exponentially sized search space, which was then given to IDP. Because this trick is not representative of how IDP is intended to be used in the real world, we decided to omit this benchmark from our experiments. Fourteen benchmark families remained with each (close to) thirty instances. They cover a wide range of applications, from a simple reachability query over a transportation planning problem to optimizing the location of valves in an urban hydraulic network.
The experimental hardware consisted of a dual-socket Intel® Xeon® E5-2698 system with 512 GiB of RAM memory, with twenty hyper-threaded cores for each of the two processors. To reduce resource competition, we run only twenty instances simultaneously, using twenty threads, for a total of ten per processor. We employ a high memory limit of 64 GiB for each instance, as we observed that Clingo requires a significant amount of memory to solve instances generated by FOLASP. 2 We run the instances with a 6000 second timeout limit, but, to avoid imprecision at the timeout limit, we consider an instance unsolved if it takes more than 5000 seconds. Optimization instances are considered solved when the last solution is proven to be optimal.
Runnable software, instance files, and detailed experimental results are made available at Zenodo. 3 We compare the efficiency of the three approaches-FOLASP, IDP and Clingo. Figure 1 (best viewed in color) shows the time needed for both FOLASP and IDP to solve each instance. For benchmarks such as nomystery, sokoban, ricochet robot and crossing minimization, the performance of FOLASP and IDP is about equal. For benchmarks such as permutation pattern matching, valves location problem, solitaire and weighted sequence, IDP clearly outperforms FOLASP. This suggests that the specifications that were hand-crafted by the IDP team are indeed well-suited to this solver's particular characteristics, and less to those of Clingo. In addition, our translation of course introduces a number of artifacts, such as reification predicates, renaming predicates and cardinality aggregates, that may adversely impact performance as well. Interestingly, however, on the graceful graphs benchmark, FOLASP clearly outperforms IDP. Here, the inefficiencies of the translation are apparently overcome by the speed of Clingo. This highlights the usefulness of a translation such as ours: different benchmarks might be more suited for the architecture of different systems.
While the above experiments used different back-ends to handle precisely the same input, our next experiments (Figure 2) use the same Clingo back-end to solve the native ASP encodings as well as the translations that are automatically generated by FOLASP from the FO(·) specification for the same benchmark. Here, we see that performance is about equal for sokoban, still life and graceful graphs. For all other benchmarks apart from nomystery, the native ASP specification significantly outperforms the automatic translation. This further confirms our ear- lier remark that the native version is able to better take advantage of the particular properties of Clingo, and that our translation's performance may suffer from the introduction of artificial predicates.
In these experiments, the nomystery benchmark is the odd one out, since the FOLASP translation here significantly outperforms the native encodings. One possible explanation for this is that the modeling style encouraged by FO(·) has computational properties different to those of typical ASP programs, and that the FO(·) style happens to be particularly well-suited to nomystery. This would again point towards the value of a translation such as ours, but now from a different perspective: it is not only useful to be able to try out different back-ends with the same specification, but it is also useful to be able to run the same back-end with specifications that were written according to different paradigms.
In our discussion of the previous experiments, we have hypothesised that the artifacts of our translation may make FOLASP's specifications harder to solve. To further investigate this, Figures 3 and 4 compare the size of the ground programs for the three approaches. This ground size is measured as the number of atoms in the ground program, for both the ASP-solving approaches (FOLASP and Clingo) and IDP, with the caveat that a ground ASP program and a ground FO(·) specification may still be quite different. For instance, IDP retains non-Boolean CP variables (De Cat et al. 2013) in its grounding, though we did switch off lazy grounding (De Cat et al. 2015).
For most benchmarks, the ground size for FOLASP is indeed significantly larger than the ground size for both IDP and Clingo. Moreover, the ground size seems to correlate roughly with performance. For instance, FOLASP outperforms IDP and Clingo on graceful graphs and nomystery, respectively, and also has the smaller ground sizes on these benchmarks. On other benchmarks, such as bottle filling or weighted sequence, FOLASP actually hit the 64 GiB memory limit during grounding.
These observations appear to confirm our hypothesis that artifacts introduced by the translation, such as auxiliary predicates, cardinality aggregates and extra rules, are a main source of poor performance. Future work may focus on how to tweak the translation such that the ground size can be reduced. 10 2 10 3 10 4 10 5 10 6 10 7 10 8 10 9 IDP3    . Scatter plot comparing Clingo and FOLASP ground size. "(x vs y)" denotes that Clingo printed a ground size for x instances, and FOLASP for y.

Conclusion
To solve real-world problems using declarative methods, both a suitable modeling language and a suitable solver are needed. The Answer Set Programming community has converged on the ASP-Core-2 standard as a common modeling language. However, while such a common language is a great driver for technological progress, it is not necessarily well-suited for all applications.
The FO(·) language may provide an interesting alternative. It builds on classical first-order logic, which may make it easier to use for domain experts who are already familiar with FO, and which may make it easier to integrate with other FO-based languages. However, it is only supported by a few solvers, which restricts the applications for which FO(·) can be used in practice.
In this paper, we aim to provide more flexibility: by presenting a translation of FO(·) model expansion problems to ASP-Core-2, we both extend the range of solvers for FO(·) and enable the use of FO(·) as an alternative modeling language for these solvers. In this way, we stimulate technological progress in solver development and in the development of applications. We implemented our approach in the FOLASP tool, which, to the best of our knowledge, is the first tool to offer a full translation from FO(·) to ASP for both model expansion and optimization.
In our experimental evaluation, we used benchmarks from the ASP competition to verify that the results computed by FOLASP are indeed correct. We also compared the performance of running Clingo on the FOLASP translation of an FO(·) specification to two alternatives: • directly running the IDP system on the FO(·) specification; • running Clingo directly on a native ASP specification.
In general, our experiments confirmed what one would typically expect, namely that the best performance is obtained by running a specification that was native to a particular solver on that solver. However, the experiments also showed that, for a number of benchmarks, our translationbased approach is actually able to match or even, in rare cases, outperform the native approaches. This demonstrates the usefulness of our translation also from a computational perspective: a specification that performs poorly with one solver, may be more efficient when translated to the input language of another solver.
Our experiments also demonstrate that, in cases where the translation performs significantly worse than the native solutions, the grounding size often appears to play an important role. Future work will therefore focus on further optimising the translation to reduce the overhead it introduces.
In summary, the main contribution of our work is to provide increased flexibility, both in choice of specification language and in choice of solver. We believe that this will be useful to drive technological progress, to develop real-world applications using the best tools for the job, and to allow cross-fertilisation between different research groups.