Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

Keywords: •, P dr Γ, N, [N] ⊢ Q - Γ, N, • ⊢ •, Q -dl

Given a logic program that is terminating and mode-correct in an idealized Prolog interpreter (i.e., in a top-down logic programming engine), a bottom-up logic programming engine can be used to compute exactly the same set of answers as the top-down engine for a given mode-correct query by rewriting the program and the query using the Magic Sets Transformation (MST). In previous work, we have shown that focusing can logically characterize the standard notion of bottom-up logic programming if atomic formulas are statically given a certain polarity assignment. In an analogous manner, dynamically assigning polarities can characterize the effect of MST without needing to transform the program or the query. This gives us a new proof of the completeness of MST in purely logical terms, by using the general completeness theorem for focusing. As the dynamic assignment is done in a general logic, the essence of MST can potentially be generalized to larger fragments of logic.

Introduction

It is now well established that two operational "dialects" of logic programming-topdown (also known as backward chaining or goal-directed) in the style of Prolog, and bottom-up (or forward chaining or program-directed) in the style of hyperresolutioncan be expressed in the uniform lexicon of polarity and focusing in the cut-free sequent calculus for a general logic such as intuitionistic logic [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF]. The difference in these diametrically opposite styles of logic programming amounts to a static and global polarity assignment to the atomic formulas. Such a logical characterisation allows a general theorem proving strategy for the sequent calculus, which might be backward (goal sequent to axioms) as in tableau methods or forward (axioms to goal sequent) like in the inverse method, to implement either forward or backward chaining (or any combination) for logic programs by selecting the polarities for the atoms appropriately. Focused inverse method provers have been built for linear logic [START_REF] Chaudhuri | The Focused Inverse Method for Linear Logic[END_REF], intuitionistic logic [START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF], bunched logic [START_REF] Donnelly | The inverse method for the logic of bunched implications[END_REF] and several modal logics [START_REF] Heilala | Bidirectional decision procedures for the intuitionistic propositional modal logic IS4[END_REF] in recent years.

The crucial ingredient for the characterisation is that polarities and focusing are sufficiently general that all static polarity assignments are complete [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF]. The two assignments may be freely mixed for different atoms, which will produce hybrid strategies. The proofs are very different: in a standard example with Fibonacci numbers, one assignment admits exponentially sized derivations, while the other has only the linear proofs. Even more importantly, the search space for proofs is wildly different for different assignments. Which static assignment to pick is not always obvious and very difficult to perform automatically, as was noted in the experiments in [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF].

In this paper, we propose to look at dynamic polarity assignment as a means to do better than static assignment for certain well-known classes of problems. To our knowledge, dynamic assignment of polarities has been investigated only once before [START_REF] Miller | Incorporating tables into proofs[END_REF]; however, the notion of assignment there is a means of incorporating tables into proof objects using new atomic cut rules with asymmetric assignments to the cut atoms. Our proposal, in contrast, retains the same inference rules as ordinary focusing, but dynamically specializes them based on polarity assignments performed at runtime; this lets us reuse the strong proof-theoretic results about focusing. Note that "dynamic polarity assignment" is not a particular algorithm but a general class of approaches for controlling search behaviour. It is useful to think of it by analogy with ordering strategies in resolution theorem proving.

In particular, we give a dynamic assignment strategy that implements the effect of the so-called magic sets transformation [START_REF] Beeri | On the power of magic[END_REF][START_REF] Ullman | Principles of Database and Knowledge-base Systems[END_REF][START_REF] Mascellani | The declarative side of magic[END_REF], which is a program transformation that constrains forward chaining to have the same set of answers as backward chaining. It is difficult to show that the transformation has this intended property. Moreover, since it is a global transformation on the program, that might even (in the general case) depend on the query, it is not modular and compositional. Our proposal reconstructs magic sets and not only avoids the transformation but also characterizes them in the common lexicon of focusing and polarities. That is, the magic sets approach is just a special case of dynamic polarity assignment, in much the same way as forward and backward chaining for Horn clauses are just special cases of static polarity assignment.

We limit our attention in this paper to the focused inverse method [START_REF] Chaudhuri | The Focused Inverse Method for Linear Logic[END_REF] as the particular general search strategy for the sequent calculus. Intuitively (but not precisely; see sec. 3), this method "compiles" a clause into an inference rule as follows:

sum (s X) Y (s Z) :-sum X Y Z. -→ ⊢ sum x y z ⊢ sum (s x) y (s z)
When this inference rule is read from premise to conclusion, the interpretation is of forward chaining on the corresponding clause. Such rules can be repeatedly applied to produce an infinite number of new sequents differing only in the number of ss, which prevents saturation even for queries with a finite backward chaining search space. With such clauses, forward chaining cannot appeal to negation by failure, unlike backward chaining. We show how to use dynamic polarity assignment to instead produce a new side condition on such inference rules: the conclusion (sum (s x) y (s z)) must be negatively polarized for the rule to be applicable. The atoms are polarized negatively by carefully selecting only those atoms that are in the base of the logic program.

One important feature of this re-examination of the magic sets approach is that, because it is performed in a more general setting, we can potentially generalize it to larger fragments of logic such as the uniform fragment. As it does not change the underlying proof system, it can potentially co-exist with other strategies. For example, if the dynamic assignment algorithm gets stuck, the remaining atoms can be polarized in some other fashion and the inverse method resumed without losing completeness.

The rest of this paper is organized as follows. In sec. 2 the magic sets transformation is sketched by way of example. Section 3 then summarizes the design of the focused inverse method and static polarity assignment. Section 4 introduces dynamic polarity assignment and shows how to use it to implement the magic sets restriction (sec. 4.2). Finally, sec. 5 discusses the conclusions and scope of future work on dynamic polarity assignment.

Magic Sets Transformation

This section contains a quick overview of the magic sets transformation for logic programs. We use the "core" version presented in [START_REF] Mascellani | The declarative side of magic[END_REF], which is less general than some other designs in the literature [START_REF] Beeri | On the power of magic[END_REF][START_REF] Ullman | Principles of Database and Knowledge-base Systems[END_REF] but also easier to explain and reason about. The logic programs we will consider are made up of Horn clauses and satisfy a global wellmodedness criterion. -A goal query is well-moded iff its inputs are ground.

-A clause a 1 t 1 → • • • → a n t n → b s is well-moded iff for all i ∈ 1.
.n, the variables in the inputs of a i t i are contained in the union of the variables in the outputs of a j t j for i < j ≤ n and of the variables in the inputs of b s . -A logic program is well-moded iff every clause in it is well-moded.

The definition of well-modedness for non-unit clauses intuitively states that, in a right-to-left reading of the clause, the inputs of an atomic formula must be defined by the outputs of earlier atomic formulas and the inputs of the head. Given a well-moded program and query, every derivation of an instance of the query from the program will be ground (for the proof, see [START_REF] Apt | Reasoning about prolog programs from modes through types to assertions[END_REF]).

Consider the motivating example from [START_REF] Mascellani | The declarative side of magic[END_REF]: computing the sum of the elements of a list of natural numbers. The clauses of the program are as follows in Prolog style.

(* mode lsum = io *) lsum [] 0. lsum (X :: Y) K :-lsum Y J, sum X J K. (* mode sum = iio *) sum 0 X X. sum (s X) Y (s Z) :-sum X Y Z.

This program is well-moded because the outputs flow into the inputs from left to right in the body of the clauses. A query such as ?-lsum [1, 2, 3] X is well-moded because the input is ground, while a query such as ?-lsum X 20 is not well-moded.

To prove a well-moded query, the backward chaining or top-down logic programming approach matches the goal with the heads of the clauses in the program, and for each successful match, replaces the goal with the matched instance of the body of the clause as new subgoals. A well-moded program is said to be terminating if there are no infinite backward chaining derivations for a well-moded query.

The forward chaining or bottom-up logic programming strategy starts from the unit clauses in the program, matches the body of a clause with these clauses, and adds the most general instance of the matched head as a new clause. This is iterated until (a generalisation of) the goal query is derived. This direction is not quite as obviously goal-directed as backward chaining, but it has many fundamental merits. It builds a database of computed facts that are all mutually non-interfering, and therefore requires no backtracking or global, stateful updates. Moreover, facts and therefore derivations are implicitly shared, so the loop detection issue that plagues backward chaining does not apply here.

However, forward chaining suffers from the obvious problem that it over-approximates the query, performing a lot of wasteful search. Fortunately, it is possible to constrain forward chaining for a given program and query such that the algorithm will saturate, i.e., reach a state where no new facts can be generated, iff the query terminates in backward chaining. This is achieved by rewriting the program and the query so that the forward algorithm approximates backward search.

The common element of the approaches to constrain forward chaining is the notion of a magic set, which is an abstract representation of the base of the program [START_REF] Mascellani | The declarative side of magic[END_REF]. We shall illustrate it here with the example above. For each predicate a, a new magic predicate a ′ is added that has the same arity as the input arity of the original predicate. Then, each clause of the program is transformed to depend on the magic predicate applied to the inputs of the head. That is, we obtain the following rewritten clauses:

lsum [] 0 :-lsum' []. lsum (X :: Y) K :-lsum' (X :: Y), lsum Y J, sum X J K. sum 0 X X :-sum' 0 X. sum (s X) Y (s Z) :-sum' (s X) Y, sum X Y Z.
As there are no longer any unit clauses, forward chaining cannot begin without some additional input. This is provided in the form of the magic version of the goal query as a new unit clause: lsum' [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Apt | Reasoning about prolog programs from modes through types to assertions[END_REF][START_REF] Beeri | On the power of magic[END_REF]. Finally, clauses are added for the magic predicates to propagate information about the base. For each non-unit clause, there is one propagation rule for each predicate in the body of the clause. In this example, they are: lsum' Y :-lsum' (X :: Y). sum' X J :-lsum' (X :: Y), lsum Y J. sum' X Y :-sum' (s X) Y.

Forward chaining on this transformed program will compute the same instances of the query as backward chaining on the original program and query.

The correctness of this magic sets transformation is generally quite difficult to prove. One of the most readable proofs was provided by Mascellani et al [START_REF] Mascellani | The declarative side of magic[END_REF]; that paper also contains a fully formal definition of the transformation and a number of other examples. However, all transformational approaches suffer from the same problems outlined in the introduction: they are not modular and compositional. In the rest of the paper we will give a different explanation of the magic sets transformation that does not suffer from these problems, and is moreover manifestly correct because of general proof theoretic properties of focused sequent calculi.

The Focused Inverse Method

In this section we review the focused inverse method for intuitionistic logic. Most of the material of this section has already appeared in in [START_REF] Chaudhuri | The Focused Inverse Method for Linear Logic[END_REF][START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF][START_REF] Degtyarev | The inverse method[END_REF] and in references therefrom. Like other recent accounts of intuitionistic focusing [START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF][START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF], we adopt a polarized syntax for formulas. Intuitively, positive formulas (i.e., formulas of the positive polarity) are those formulas whose left sequent rules are invertible and negative formulas are those whose right rules are invertible. Every polarized logical connective is unambiguously in one of these two classes. In order to prevent an overlap, we also assign the atomic formulas individually to one of the two classes. Any polarity assignment for the atoms is complete [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF].

Definition 4 (syntax)

We follow this grammar:

P, Q p P ⊗ Q 1 P ⊕ Q 0 ∃x. P ↓N N, M n N & M ⊤ P ⊸ N ∀x. N ↑P p a t , + n a t , - P - P n N + N p
-Formulas (A, B, . . .) are either positive (P, Q, . . .) or negative (N, M, . . .).

-Atomic formulas (or atoms) (p, q, n, m, . . .) are also polarized. Each atom consists of an atomic predicate (a, b, . . .) applied to a (possibly empty) list of terms, and a polarity. We shall generally abuse notation and write a t , ± as a ± t , even though it is the atom and not the predicate that carries the polarity. -Left passive formulas (N + , M + , . . .) and right passive formulas (P -, Q + , . . .) are used to simplify the presentation of rules.

We use connectives from polarized linear logic instead of the more usual intuitionistic connectives to make the polarities explicit. The polarity switching connectives ↓ and ↑ are only bureaucratic and do not change the truth value of their operands. Both ⊗ and & have the same truth value as the usual intuitionistic conjunction ∧-that is, A ⊗ B ≡ A & B if we ignore polarities and omit the switching connectives ↓ and ↑-just different inference rules. In other formulations of polarized intuitionistic logic these two polarisations of conjunction are sometimes written as ∧ + or ∧ - [START_REF] Liang | A unified sequent calculus for focused proofs[END_REF], but we prefer the familiar notation from linear logic. Likewise, ⊕ has the same truth value as ∨ and ⊸ the same truth value as →.

The inference system for this logic will be given in the form of focused sequent calculus rules [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF]. We have the following kinds of sequents: where: Γ Fig. 1. Focused sequent calculus for polarized first-order intuitionistic logic. In the rules ∃l a and ∀r a the parameter a is not free in the conclusion. The focused sequent calculus will be presented in a stylistic variant of Andreoli's original formulation [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF]. The full set of rules is in fig. 1. It has an intensional reading in terms of phases. At the boundaries of phases are sequents of the form Γ ; • ⊢ • ; Q -, which are known as neutral sequents. Proofs of neutral sequents proceed (reading from conclusion to premises) as follows:

Γ ⊢ [P] right-focus on P Γ ; [N] ⊢ Q -left-focus on N Γ ; Ω ⊢        N ; • • ; Q - γ left-
Γ, N, p ⊢ p pr Γ, N, p ⊢ p ⊕ q Γ, N, p ; • ⊢ • ; l Γ, N, p ; • ⊢ l ; • Γ, N, p ⊢ [↓l] Γ, N, p ; [n] ⊢ n nl Γ, N, p ; [↓l ⊸ n] ⊢ n Γ, N, p ; [m & (↓l ⊸ n)] ⊢ n &l 2 Γ, N, p ; [N] ⊢ n Γ, N, p ; • ⊢ • ; n dl i.e., Γ, N, p ; • ⊢ • ; l Γ, N, p ; • ⊢ • ; n
1. Decision: a focus is selected from a neutral sequent, either from the passive context or from the right. This focused formula is moved to its corresponding focused zone using one of the rules dl or dr (d = "decision", and r/l = "right"/"left"). The left rule copies the focused formula.

2. Focused phase: for a left or a right focused sequent, left or right focus rules are applied to the formula under focus. These focused rules are all non-invertible in the (unfocused) sequent calculus-that is, they can fail to apply-and therefore depend on essential choices made in the proof. This is familiar from focusing for linear logic [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF].

3. Active phase: once the switch rules ↓r and ↑l are applied, the sequents become active and active rules are applied. The order of the active rules is immaterial as all orderings will produce the same list of neutral sequent premises. In Andreoli's system the irrelevant non-determinism in the order of these rules was removed by treating the active context Ω as ordered; however, we do not fix any particular ordering.

The soundness of this calculus with respect to an unfocused sequent calculus, such as Gentzen's LJ, is obvious. For completeness, we refer the interested reader to a number of published proofs in the literature [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF][START_REF] Miller | From proofs to focused proofs: a modular proof of focalization in linear logic[END_REF][START_REF] Howe | Proof Search Issues in Some Non-Classical Logics[END_REF].

The purpose of starting with a polarized syntax and a focused calculus is that we are able to look at derived inference rules for neutral sequents as the basic unit of steps. For instance, one of the derived inference rules for the formula N p ⊕ q ⊸ m & (↓l ⊸ n) in the passive context is given in fig. 2. The instance of pr above forces p to be in the passive context because that is the only rule that can be applied to contruct a sequent of the form ∆ ⊢ p . Likewise, the nl rule forces the right hand side of the conclusion sequent to be the same as the left focused atom n. Finally, the dl rule requires N to already be present in the passive context.

As we observe, focusing compiles formulas such as N above, which may be clauses in a program, into (derived) inference rules. Focusing can also produce new facts, which are neutral sequents that have no open premises after applying a derived inference rule. An example would be the case for the derivation above where, instead of &l 2 we were to use &l 1 . In this case we would obtain the fact Γ, N, p ; • ⊢ • ; m. If the goal were of this form, we would be done.

This property of focusing can be exploited to give a purely proof-theoretic explanation for certain dialects of proofs. For Horn clauses, consider the case where all the atoms are negative, i.e.clauses are of the form ∀ x . ↓m 1 ⊸ • • • ⊸ ↓m j ⊸ n. If clause were named N, then its derived inference rule is:

Γ, N ; • ⊢ • ; m 1 [ t / x ] • • • Γ, N ; • ⊢ • ; m j [ t / x ] Γ, N ; • ⊢ • ; n[ t / x ]
Since the context is the same in all premises and the conclusion, we need only look at the right hand side. If we read the rule from conclusion to premises, then this rule implements back-chaining from an instance of the head of this Horn clause to the corresponding instances of the body of the clause, where the neutral sequents represent the current list of sub-goals. Thus, the general top-down logic programming strategy (or backward chaining) consists of performing goal-directed focused proof search on Horn clauses with negative atoms. If the atoms were all assigned positive polarity instead, then the same goal-directed focused proof search would perform a kind of bottom-up logic programming (or forward chaining). Static polarity assignment for the atoms is therefore a logical characterisation of forward and backward chaining strategies. Indeed, if the atoms were not uniformly given the same polarities, then the focused proofs would be a mixture of forward and backward chaining.

Forward reasoning and the inverse method

An important property of the (cut-free) sequent calculus of fig. 1 is that there is a structural cut-elimination algorithm [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF]; as a consequence, the calculus enjoys the subformula property. Indeed, it is possible to state the subformula property in a very strong form that also respects the sign of the subformula (i.e., whether it is principal on the left or the right of the sequent) and the parametricity of instances (i.e., the subformulas of a right ∀ or a left ∃ can be restricted to generic instances). We omit a detailed definition and proof here because it is a standard result; see e.g. [START_REF] Chaudhuri | A focusing inverse method theorem prover for first-order linear logic[END_REF] for the definition. With the strong subformula property, we can restrict the rules of fig. 1 to subformulas of a given fixed goal sequent. It then becomes possibile to apply the inference rules in a forward manner, from premises to conclusion. The inputs of such a forward reasoning strategy would be the facts that correspond to focusing on the passive formulas and operands of the switch connectives in the goal sequent, subject to the subformula restriction. That is, the initial sequents (in the rules pr and nl) correspond to atomic formulas that are both a left and a right signed subformula of the goal sequent. From these initial sequents we apply the (subformula-restricted) inference rules forward until we derive (a generalisation of) the goal sequent. In order to implement the calculus, the axiomatic rules such as 1r are refined to omit the passive context; the additive rules are turned into multiplicative rules and an explicit rule of factoring added; and the calculus is lifted to free variables with identity replaced with unifiability, and only most general instances are considered. This core "recipe" is outlined in the Handbook article on the inverse method [START_REF] Degtyarev | The inverse method[END_REF] and is not repeated here.

One optimisation not mentioned in [START_REF] Degtyarev | The inverse method[END_REF] but implemented in many inverse method provers [START_REF] Chaudhuri | The Focused Inverse Method for Linear Logic[END_REF][START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF] is globalisation: the forward version of the dl rule is specialized into the following two forms:

Γ ; [N] ⊢ Q -N Γ 0 Γ, N ; • ⊢ • ; Q - dlf 1 Γ ; [N] ⊢ Q -N ∈ Γ 0 Γ ; • ⊢ • ; Q - dlf 2
where Γ 0 is the passive context of the goal sequent. This context is present in every sequent in the backward proof, so there is no need to mention it explicitly in the forward direction. For logic programs, Γ 0 will contain the clauses of the program and it is not important to distinguish between two computed sequents that differ only in the used clauses of the program.

Let us revisit the static polarity assignment question in the forward direction. The forward derived rule for the Horn clause ∀ x . ↓m 1 ⊸ • • • ⊸ ↓m j ⊸ n ∈ Γ 0 , after lifting to free variables, is:

Γ 1 ; • ⊢ • ; m ′ 1 • • • Γ j ; • ⊢ • ; m ′ j θ = mgu( m 1 , . . . , m j , m ′ 1 , . . . , m ′ j ) (Γ 1 , . . . , Γ n ; • ⊢ • ; n)[θ]
For unit clauses, which provide the initial sequents, the passive context Γ is empty (because there are no premises remaining after globalisation). Therefore, all neutral sequents computed by forward reasoning will have empty passive contexts, giving us the rule:

• ; • ⊢ • ; m ′ 1 • • • • ; • ⊢ • ; m ′ j θ = mgu( m 1 , . . . , m j , m ′ 1 , . . . , m ′ j ) (• ; • ⊢ • ; n)[θ]
Thus, this derived inference rule implements forward chaining for this clause. This situation is dual to the backward reading of the rules of fig. 1 where a static negative assignment to the atoms implemented backward chaining. As expected, a static positive polarity assignment to the atoms implements backward chaining in the forward calculus. The technical details of operational adequacy can be found in [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF].

Dynamic Polarity Assignment

The previous section demonstrates that we can implement forward chaining (or bottom up logic programming) using the vocabulary of focusing and polarity assignment. For the rest of this paper we shall limit or attention to forward reasoning as the global strategy, with negative polarity assignment for the atoms as our means of implementing forward chaining.

Obviously the benefit of polarity assignment is that completeness is a trivial consequence of the completeness of focusing with respect to any arbitrary, even heterogeneous, polarity assignment for the atoms. Moreover, the completeness of the inverse method merely requires that the rule application strategy be fair. This minimal requirement of fairness does not force us to assign the polarity of all atoms statically, as long as we can guarantee that every atom that is relevant to the proof is eventually assigned a polarity (and that the rest of the inverse method engine is fair). Can we do better than static assignment with dynamic assignment? This section will answer this question affirmatively.

The mechanism of dynamic polarity assignment

Let us write unpolarized atoms (i.e., atoms that haven't been assigned a polarity) simply in the form a t, and allow them to be used as both positive and negative formulas in the syntax. That is, we extend the syntax as follows:

P, Q, . . . a t p P ⊗ Q 1 P ⊕ Q 0 ∃x. P ↓N N, M, . . . a t n N & M ⊤ P ⊸ N ∀x. N ↑P
For example, A Horn clause with unpolarized atoms have the syntax ∀ x. a 1 t 1 ⊸ • • • ⊸ a j t j ⊸ b s where the x are the variables that occur in the terms t 1 , . . . , t j , s. Consider a variant of the focused inverse method where we allow two kinds of sequents as premises for inference rules: neutral sequents, as before, and sequents that have a focus on an unpolarized atom which we call proto sequents. An inference rule with proto sequent premises will be called a proto rule.

Definition 5

Environments (E, F , . . .) are given by the following grammar:

E, . . . P Q P, Q, . . . P ⊗ Q P ⊗ Q P ⊕ Q P ⊕ Q ∃x. P ↓N N, M, . . . N & M N & M P ⊸ N P ⊸ N ∀x. N ↑P
We write E(A) for the formula formed by replacing the in E with A, assuming it is syntactically valid. An environment E is called positive (resp. negative) if E(p) (resp. E(n)) is syntactically valid for any positive atom p (resp. negative atom n).

Definition 6 (polarity assignment) We write A[a t ← +] (resp. A[a t ← -]) to stand for the positive (resp. negative) polarity assignment to the unpolarized atom a t in the formula A. It has the following recursive definition:

-If the unpolarized atom a t does not occur in A, then A[a t ← ±] = A.

-

If A = E(a t ) and E is positive, then A[a t ← +] = (E(a + t ))[a t ← +] A[a t ← -] = (E(↓a -t ))[a t ← -] -If A = E(a t ) and E is negative, then A[a t ← +] = (E(↑a + t ))[a t ← +] A[a t ← -] = (E(a -t ))[a t ← -]
This definition is extended in the natural way to contexts, (proto) sequents, and (proto) rules.

Polarity assignment on proto rules generally has the effect of instantiating certain schematic meta-variables. For instance, consider the following proto-rule that corresponds to a left focus on the unpolarized Horn clause C ∀x, y. a x ⊸ b y ⊸ c x y:

Γ, C ⊢ [a s] Γ, C ⊢ [b t] Γ, C ; [c s t] ⊢ Q - Γ, C ; • ⊢ • ; Q -
All the premises of this rule are proto sequents. Suppose we assign a positive polarity to a s; this will change the proto rule to:

Γ, C ⊢ [a + s] Γ, C ⊢ [b t] Γ, C ; [c s t] ⊢ Q - Γ, C ; • ⊢ • ; Q - (where C ′ is C[a s ← +]
). This proto rule actually corresponds to:

Γ, C ′ , a + s ⊢ [b t] Γ, C ′ , a + s ; [c s t] ⊢ Q - Γ, C ′ , a + s ; • ⊢ • ; Q -
because the only way to proceed further on the first premise is with the pr rule. This instantiates Γ with Γ, a + s. If we now assign a negative polarity to c s t, we would obtain the rule:

Γ, C ′′ , a + s ⊢ [b t] Γ, C ′′ , a + s ; • ⊢ • ; c -s t (where C ′′ = C ′ [c s t ← -]) which instantiates Q -to c -s t.
Finally, if we assign a negative polarity to b t, we would obtain the ordinary (non-proto) inference rule with neutral premise and conclusion:

Γ, C ′′′ , a + s ; • ⊢ • ; b -t Γ, C ′′′ , a + s ; • ⊢ • ; c -s t (where C ′′′ = C ′′ [b t ← -]).

Implementing magic sets with dynamic polarity assignment

This sub-section contains the main algorithm of this paper -a dynamic polarity assignment strategy that implements magic sets in the inverse method. The key feature of the algorithm is that it involves no global rewriting of the program clauses, so soundness is a trivial property. Completeness is obtained by showing that the algorithm together with the inverse method performs fairly on well-moded logic programs and queries.

The algorithm consists of dynamically assigning negative polarity to unpolarized atoms. Initially, all atoms in the program are unpolarized and the atom in the goal query is negatively polarized. It maintains the following lists:

-Seeds, which is a collection of the negatively polarized atoms; -Facts, which is a list of computed facts which are ordinary neutral sequents; -Rules, which is a list of partially applied, possibly proto, rules. Whenever a fact is examined by the inner loop of the inverse method, new facts and partially applied (possibly proto) rules are generated. After the inner loop ends (i.e., after all subsumption checks and indexing), the following seeding step is repeatedly performed until quiescence. Definition 7 (seeding step) For every right-focused proto-sequent in the premise of every proto rule, if the focused atom is mode correct-that is, if the input arguments of the atom are ground-then all instances of that atom for arbitrary outputs are assigned a negative polarity. These new negatively polarized atoms are added to the Seeds.

For example, if the unpolarized atom sum 3 4 ( f (x)) has a right focus in a proto rule and sum has mode iio, then all atoms of the form sum 3 4 _ are assigned negative polarity. The seeding step will generate new facts or partially applied rules, which are then handled as usual by the inverse method.

Example

Let us revisit the example of sec. 2. Let Π 0 be the collection of unpolarized Horn clauses representing the program, i.e.:

Π 0 = lsum [] 0, (C 1 ) ∀x, y, j, k. lsum y j ⊸ sum x j k ⊸ lsum (x :: y) k, (C 2 ) ∀x. sum 0 x x, (C 3 ) ∀x, y, z. sum x y z ⊸ sum (s x) y (s z) (C 4 )
As before, let the modes be io for lsum and iio for sum. The above program is terminating and mode-correct for this moding. Consider the query lsum [1, 2, 3] X, i.e., we are proving the goal sequent:

The rule (C 2111 ) produces a seed lsum -[] _ that matches the premise of (C 1 ) to produce our first fact: • ; • ⊢ • ; lsum -[] 0. This can now be applied in the premise of (C 2111 ) by the inverse method loop to produce the following partially applied instance:

Γ ⊢ [sum 3 0 k] Γ ; • ⊢ • ; lsum -[3] k (C 5 )
This finally gives us our first seed for sum, viz. sum -3 0 _. This seed will, in turn produce seeds sum -2 0 _, sum -1 0 _, and sum -0 0 _ from instances of the rule (C 4 ). The last of these seeds will instantiate (C 3 ) to give our second fact, • ; • ⊢ • ; sum -0 0 0. The inverse method will then be able to use this rule to partially apply the instances of the (C 3 ) rule to produce, eventually, • ; • ⊢ • ; sum -3 0 3, which can be matched to (the instance of) (C 5 ) to give our second derived fact about lsum, viz. • ; • ⊢ • ; lsum -[3] 3. These steps repeat twice more until we eventually derive • ; • ⊢ • ; lsum -[1, 2, 3] 6, which finally lets us derive the goal sequent using (the instance of) (g).

Correctness

Crucially, no further inferences are possible in the example of the previous section. There will never be any facts generated about lsum -[5, 1, 2, 3, 4] x, for instance, because there is never a seed of that form. Thus, as long as there is a well-founded measure on the seeds that is strictly decreasing for every new seed, this implementation of the inverse method will saturate.

Lemma 8 (seeding lemma) All atoms occurring to the right of sequents in the Facts list are instances of atoms in the Seeds.

Proof. Since the only polarity assignment is to assign an unpolarized atom the negative polarity, the only effect it has on proto inference rules is to finish left-focused proto sequent premises with nl, and turn right-focused proto sequent premises into neutral sequent premises. Finishing the left-focused premises has the side effect of instantiating the right hand side with the newly negatively polarized atom. If there are no neutral premises as a result of this assignment, then the newly generated fact satisfies the required criterion. Otherwise, when the conclusion is eventually generated by applying the rule in the inverse method, the right hand side will be an instance of the negatively polarized atom.

⊓ ⊔

The main result of this paper is a simple corollary.

Corollary 9 (saturation) Given a well-moded logic program that terminates on all well-moded queries-i.e., all derivations of a well-moded query are finite-the inverse method with the dynamic polarity assignment algorithm of sec. 4.1 saturates for all well-moded queries.

Proof (Sketch). Instead of giving a fully formal proof, which is doable in the style of [START_REF] Mascellani | The declarative side of magic[END_REF], we give only the intuition for the proof. Note that if the logic program is terminating for all well-moded queries, then there is a bounded measure | | that is strictly decreasing from head to body of all clauses in the program. We use this measure to build a measure on the Seeds collection as follows:

-For each atom in Seeds, pick the element with the smallest | |-measure.

-For each atom not in Seeds, pick greatest lower bound of the | |-measure.

-Pick a strict but arbitrary ordering of all the predicate symbols and arrange the measures selected in the previous two steps in a tuple according to this ordering. This tuple will be the measure of Seeds.

It is easy to see that this measure on Seeds has a lower bound according to the lexicographic ordering. Therefore, all we need to show is that this measure is decreasing on Seeds for every seeding step and then we can use lem. 8 to guarantee saturation. But this is easily shown because the | |-measure decreases when going from the conclusion to the premises of every derived inference rule for the clauses of the logic program (see the example in sec. 4.3).

⊓ ⊔

The completeness of the dynamic polarity assignment algorithm follows from the completeness of focusing with (arbitrary) polarity assignment, the completeness of the inverse method given a fair strategy, and the observation that Seeds contains a superset of all predicates that can appear as subgoals in a top-down search of the given logic program.

Conclusion

We have shown how to implement the magic sets constraint on a focused forward search strategy by dynamically assigning polarities to unpolarized atoms. As one immediate consequence, our forward engine can respond with the same answer set as traditional back-chaining for well-moded and terminating programs. The notion of dynamic polarity assignment is novel to this work and the last word on it is far from written. The obvious next step is to see how it generalizes to fragments larger than Horn theories. More fundamentally, while fairness in the inverse method gives a general external criterion for completeness, an internal criterion for judging when a given dynamic polarity assignment strategy will be complete is currently missing.

  active on Ω and right-active on N

Fig. 2 .

 2 Fig. 2. One derived inference rule for N.

Definition 1 (abstract syntax of Horn clauses) A Horn clause

  Note that the clause a :-b, ..., z in a Prolog-like concrete syntax would be written as z → • • • → b → a in the above abstract syntax that is, the order of the clauses in the body is reversed. Many extensions of this definition of Horn clauses exist in the literature, but they are all generally equivalent to this fragment. A logic program is an unordered collection of Horn clauses where each predicate and function symbol has a unique arity. (We do not consider particular orderings of the clauses because we are not interested in the operational semantics of a particular logic programming language.)

				is an iterated implica-
	tion of atomic formulas that is implicitly universally closed over all its variables. That
	is, Horn clauses (C, D, . . .) satisfy the following grammar:
	C, D, . . .	a t a t → C	t, s, . . .	x f t
	where a ranges over predicate symbols, f over function symbols, and x over variables.
	The notation t stands for a list, possibly empty, of terms.
	Definition 2 (moding) Every predicate symbol of arity n can be assigned a mode,
	which is a string of length n composed of the characters i and o, which are mnemonics
	for "input" and "output" respectively. A mode assignment to all predicates in a logic
	program is called a moding. The inputs of a predicate with respect to a mode are those
	arguments corresponding to the occurrences of i in the mode; likewise, the outputs are
	the arguments corresponding to o in the mode.

Definition 3 (well-modedness) All the following are with respect to a given moding:

• Γ, N -is called the passive context and Ω • Ω, P is the active context. Both contexts are interpreted as multisets (admits only exchange). We adopt the usual convention of denoting multiset union with commas. It will turn out that the passive context is also a set, but this is an admissible principle and does not depend on primitive weakening and contraction rules. Note therefore that Γ 1 , Γ 2 is not the same as Γ 1 ∪ Γ 2 ; if the latter interpretation is needed, it will be written explicitly.(active) Γ ; Ω ⊢ • ; n Γ ; Ω ⊢ n ; • nr Γ ; Ω ⊢ • ; P Γ ; Ω ⊢ ↑P ; • ↑r Γ ; Ω ⊢ N ; • Γ ; Ω ⊢ M ; • Γ ; Ω ⊢ N & M ; • &r Γ ; Ω ⊢ ⊤ ; • ⊤r Γ ; Ω, P ⊢ N ; • Γ ; Ω ⊢ P ⊸ N ; • ⊸r Γ ; Ω ⊢ N[a/x] ; • Γ ; Ω ⊢ ∀x. N ; • ∀r a Γ, p t ; Ω ⊢ γ Γ ; Ω, p t ⊢ γ pl Γ, N ; Ω ⊢ γ Γ ; Ω, ↓N ⊢ γ ↓l Γ ; Ω, P, Q ⊢ γ Γ ; Ω, P ⊗ Q ⊢ γ ⊗l Γ ; Ω ⊢ γ Γ ; Ω, 1 ⊢ γ 1l Γ ; Ω, P ⊢ γ Γ ; Ω, Q ⊢ γ Γ ; Ω, P ⊕ Q ⊢ γ ⊕l Γ ; Ω, 0 ⊢ γ 0l Γ ; Ω, N[a/x] ⊢ γ Γ ; Ω, ∃x. N ⊢ γ ∃l a (right focus) Γ, p ⊢ p pr Γ ; • ⊢ N ; • Γ ⊢ [↓N] ↓r Γ ⊢ [P] Γ ⊢ [Q] Γ ⊢ [P ⊗ Q] ⊗r Γ ⊢ [1] 1r Γ ⊢ [P i ] Γ ⊢ [P 1 ⊕ P 2 ] ⊕r i Γ ; [P[t/x]] Γ ⊢ [∃x. P] ∃r (left focus) Γ ; [n] ⊢ n nl Γ ; P ⊢ • ; Q - Γ ; [↑P] ⊢ Q -↑l Γ ; [N i ] ⊢ Q - Γ ; [N 1 & N 2 ] ⊢ Q -&l i Γ ⊢ [P] Γ ; [N] ⊢ Q - Γ ; [P ⊸ N] ⊢ Q -⊸l

Π 0 , ∀x. lsum[START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Apt | Reasoning about prolog programs from modes through types to assertions[END_REF][START_REF] Beeri | On the power of magic[END_REF] x ⊸ g Γ 0 ; • ⊢ • ; g Since there are no switched subformulas, the only available rules will be for clauses in Γ 0 and the goal g. Using the subformula restriction and globalisation, we would then obtain the following derived proto rules:Γ ; [lsum [] 0] ⊢ Q - Γ ; • ⊢ • ; Q - (C 1 ) Γ 1 ; lsum (x :: y) k ⊢ Q -Γ 2 ⊢ lsum y j Γ 3 ⊢ sum x j k Γ 1 , Γ 2 , Γ 3 ; • ⊢ • ; Q - (C 2 ) Γ ; [sum 0 x x] ⊢ Q - Γ ; • ⊢ • ; Q - (C 3 ) Γ 1 ; sum (s x) y (s z) ⊢ Q -Γ 2 ⊢ sum x y z Γ 1 , Γ 2 ; • ⊢ • ; Q - (C 4 ) Γ 1 ; [g] ⊢ Q -Γ 2 ⊢ [lsum [1, 2, 3] x] Γ 1 , Γ 2 ; • ⊢ • ; Q - (g)There are no initial sequents, so we perform some seeding steps. The initial polarity assignment is negative for the goal g; this produces the following instance of (g):Γ 2 ⊢ [lsum [1, 2, 3] x] Γ ; • ⊢ • ; g - (g ′ )Now we have a right focus on a well-moded unpolarized atom, viz. lsum[START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Apt | Reasoning about prolog programs from modes through types to assertions[END_REF][START_REF] Beeri | On the power of magic[END_REF] x, so we add lsum -[1, 2, 3] _ to the Seeds. This produces two instances of the proto rule (C 2 ) depending on the two ways in which the seed can match the proto premises.Γ 1 ⊢ lsum [2, 3] j Γ 2 ⊢ sum 1 j k Γ 1 , Γ 2 ; • ⊢ • ; lsum -[1, 2, 3] k (C 21 ) Γ 1 ; [lsum (x :: [1, 2, 3]) k] ⊢ Q -Γ 2 ; • ⊢ • ; lsum -[1, 2, 3] j Γ 3 ⊢ sum x j k Γ 1 , Γ 2 , Γ 3 ; • ⊢ • ; Q - (C 22 )The first premise in (C 21 ) is well-moded and will produce further seeds. However, (C 22 ) produces no seeds as there are no proto premises with a right focus on a well-moded unpolarized atom. Continuing the seeding steps for (C 21 ) we produce the following new useful proto rules:Γ 1 ⊢ lsum [2] j Γ 2 ⊢ sum 2 j k Γ 1 , Γ 2 ; • ⊢ • ; lsum -[2, 3] k (C 211 ) Γ 1 ⊢ lsum [] j Γ 2 ⊢ sum 3 j k Γ 1 , Γ 2 ; • ⊢ • ; lsum -[3] k (C 2111 )

Acknowledgement: We thank Brigitte Pientka for several useful discussions about magic sets and polarity assignment.


Samer Lahoud
email: samer.lahoud@enst-bretagne.fr

Géraldine Texier
email: geraldine.texier@enst-bretagne.fr

Laurent Toutain
email: laurent.toutain@irisa.fr

Flow Allocation with Path Protection in Next Generation Internet Networks

In this work, we study the flow allocation problem in Next Generation Internet (NGI) networks. Given a capacitated network, flow allocation consists of a simultaneous routing and bandwidth allocation problem for flows realizing a set of sourcedestination demands. We consider the case where demands are elastic and the flow realizing one demand can be arbitrary split over multiple paths. Moreover, we ensure that the allocated flows are survivable to network failures using path protection. We investigate the possibility of sharing backup capacity, thus enabling more efficient resource consumption. Depending on the optimization objective, we provide two different approaches to the problem. The first approach maximizes the total allocated volume and the second one maximizes the minimum allocated volume. We build mathematical formulations based on generalizations of the maximum multicommodity flow and the maximum concurrent flow problems. Moreover, we provide new approximation algorithms based on a primal-dual approach. These algorithms compute a solution that is within a guaranteed factor of the optimal. Numerical results enable to get deeper insights on the quality and compared performance of the different approaches.

I. INTRODUCTION

Once capacities have been assigned to the Next Generation Internet (NGI) core links in the capacity design phase, network engineers can tackle the flow allocation problem. The challenge is to determine how much traffic of each demand should be admitted in the network and how this traffic should be routed in order to satisfy the requirement of high network utilization while guaranteeing fairness to the users. Thus, the optimization objective of the flow allocation problem depends on the provisioning strategy chosen by network engineers. Moreover, survivability requirements are introduced at this level of the network optimization. Backup capacity is provisioned in order to provide protection for allocated flows against network failures. Hence, considering both the provisioning strategy and the survivability mechanism, we end up with various formulations for the flow allocation problem. In this work, we study the survivable flow allocation problem with dedicated and shared path protection. We consider the case where demands are elastic, in the sense that they can employ any volume of resources they are assigned, and the flow realizing one demand can be arbitrary split over multiple paths. The main contribution of this paper is to provide two different formulations illustrating different provisioning strategies. The first approach maximizes the total allocated volume, given by the sum of allocated flows for all demands. The second approach maximizes the minimum allocated volume. We build mathematical formulations based on generalizations of the maximum multicommodity flow and the maximum concurrent flow problems. Moreover, we provide new approximation algorithms based on a primal-dual approach. These algorithms compute a solution that is within a guaranteed factor of the optimal. Our paper is organized as the following: in Section II, we introduce the context of our work, emphasizing the provisioning strategies and the survivability requirements. Then, in Section III, we present the mathematical formulation and the corresponding notation of the survivable flow allocation problems. In Section IV, we provide the approximation algorithms that compute efficient solutions to the problems presented in Section III. Moreover, we present an overview over the related work in section V. Finally, in Section VI, we present relevant simulation results, and conclude in Section VII with insights on our future work.

II. CONTEXT AND MOTIVATION

In this section, we review the major key elements involved in the survivable flow allocation problem. We briefly present the survivability mechanisms and the provisioning strategies in use.

a) Survivability: NGI network operators are more and more solicited to ensure a minimal level of service disruption during network failures. This requirement can be specified as part of an extended Service Level Agreement (SLA). Moreover, many mechanisms have been developed in order to satisfy the survivability requirement. Generally speaking, protection mechanisms consist in provisioning backup capacity that can be used by the failed traffic in order to survive the failure. These mechanisms can be broadly classified into link protection and path protection. In the link protection mechanism, the protected entity is one single link. A backup path is provided to recover the traffic on a failed link. In the path protection mechanism, used in this work, the protected entity, called primary path, spans from the source node to the destination node. A backup path is provided to recover the failed traffic on the primary path, when any of its links fails. Primary and backup paths must be link disjoint, so that no single link failure can affect both paths. Moreover, node failures can be taken into account by requiring node disjointness.

Path protection provides good utilization of backup resources compared to link protection where the protected entity is a single link. However, timeliness of path protection can become a real issue as the switching between primary and backup resources is done at the source node. Protection mechanisms can also be classified according to the allocation type of the backup resources. Therefore, two types of protection are defined dedicated and shared protection. The difference between the two lies in whether or not resource sharing is possible between different protection paths. The idea is to share the backup resources between protected entities that are not affected in the same failure situation. In dedicated protection, a protecting entity is dedicated to one single protected entity. This results in a very fast restoration service while the ratio of redundancy (i.e., the ratio of capacity taken by protection and working paths in the network) usually reaches 100% [START_REF] Ho | On achieving optimal survivable routing for shared protection in survivable next-generation internet[END_REF]. On the other hand, shared protection can substantially reduce the ratio of redundancy required to achieve 100% restorability at the expense of a little longer restoration time.

b) Provisioning Strategies: With the rapid growth of Internet traffic, the simple over-provisioning has become less economical. Therefore, one big challenge for network engineers is to determine how much traffic of each demand should be admitted to the network and how this traffic should be routed in order to satisfy the requirement of high network utilization and to guarantee fairness to the users. One simple strategy consists in maximizing the total admitted traffic. This approach ensures maximum resource utilization. However, it does not guarantee any fairness between different demands. This becomes a real issue when demands belong to different users and allocated volumes can influence their satisfaction. Hence, another strategy consists in maximizing the minimum allocated volume for all demands, thus ensuring simple fairness between the demands.

III. NOTATION AND PROBLEM FORMULATION

In the following, we consider a capacitated network represented by an undirected graph G = (V, E) with V being the set of vertices (|V| = V ) and E the set of links (|E| = E). The capacity for each e ∈ E is denoted by C e . This is the total bandwidth that can be routed on link e. Moreover, we denote by D the set of directed demands (|D| = D). The allocated volume for demand d is realized by means of a survivable flow allocated to cycles joining the source and the destination node of demand d. The cycle set corresponding to demand d is denoted by K d and includes K d pairs of link-disjoint paths. This ensures the flow survivability under single link failures. Particularly, the cycle incidence relation is represented by the constant α edk that equals 1 if link e belongs to cycle k ∈ K d realizing demand d and 0, otherwise. Moreover, the flow realizing demand d and allocated to cycle k is denoted by f dk .

A. Flow Allocation with Dedicated Path Protection

In this section, we provide two different formulations for the flow allocation problem with Dedicated Path Protection (DPP) each one realizing a different optimization objective.

LP 1 MS-DPP Maximize

d∈D k∈K d f dk (1)
Subject to:

d∈D k∈K d α edk f dk ≤ C e , ∀e ∈ E (2)
f dk ≥ 0, ∀d ∈ D, ∀k ∈ K d (3)

1) Maximizing the Total Allocated Volume:

The first approach, referred to as MS-DPP, maximizes the total allocated volume. The correspondent mathematical problem is presented in LP 1. This problem is a generalization of the maximum multicommodity flow. Using the notation introduced above, the objective of the problem expressed in (1) consists in maximizing the sum of the cycle flow values f dk , for all the demands and all the cycles realizing these demands respectively. Moreover, constraint [START_REF] Fleischer | Approximating fractional multicommodity flow independent of the number of commodities[END_REF] ensures that the allocated traffic on link e (∀e ∈ E) does not exceed its capacity.

2) Maximizing the Minimum Allocated Volume: The second approach, referred to as MM-DPP, maximizes the minimum allocated volume. The correspondent mathematical problem is presented in LP 2. This problem is a generalization of the maximum concurrent flow. The objective, expressed in (4), consists in maximizing the minimum allocated volume for all demands. This minimum allocated volume is denoted by F and verifies constraint [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF]. Moreover, constraint [START_REF] Hauser | Capacity design of fast path restorable optical networks[END_REF] ensures that the allocated traffic on link e (∀e ∈ E) does not exceed its capacity.

LP 2 MM-DPP Maximize F (4)
Subject to:

k∈K d f dk ≥ F, ∀d ∈ D ( 5
)
d∈D k∈K d α edk f dk ≤ C e , ∀e ∈ E ( 6
)
f dk ≥ 0, ∀d ∈ D, ∀k ∈ K d (7)

B. Flow Allocation with Shared Path Protection

In order to add sharing to the flow allocation problems, we consider S single failure scenarios where s = 0 is the non failure situation and 1 ≤ s ≤ S corresponds to the failure of link e where e = s (we get S = 1 + E). Moreover, θ dks denotes the availability of the primary path in cycle k ∈ K d realizing demand d under situation s. Hence, θ dks equals 1 if the primary path of cycle k is available in situation s (i.e. all the links in this path are available) and 0, otherwise. We introduce new constants: α p edk (resp. α b edk ) that equals 1 if link e belongs to the primary (resp. backup) path of cycle k ∈ K d realizing demand d and 0, otherwise. For a compact notation, we will use θdks to denote the value of 1θ dks .

LP 3 MS-SPP Maximize d∈D k∈K d f dk (8)
Subject to:

d∈D k∈K d (θ dks α p edk + θdks α b edk )f dk ≤ C e , ∀e ∈ E, ∀s ∈ S (9) f dk ≥ 0, ∀d ∈ D, ∀k ∈ K d (10)
1) Maximizing the Total Allocated Volume: MS-SPP is obtained by modifying the capacity constraint (2) in the dedicated version of the problem. Now, under situation s, the total flow on link e is given by the sum of the working flows on link e that are available under situation s and the backup flows that are activated under the same situation (i.e. recovering the failing working flows). This total flow must not exceed the capacity of link e under any situation s. Hence the new capacity constraint is given in (9) and the problem formulation in LP 3.

LP 4 MM-SPP

Maximize F (11) Subject to:

k∈K d f dk ≥ F, ∀d ∈ D (12) d∈D k∈K d (θ dks α p edk + θdks α b edk )f dk ≤ C e , ∀e ∈ E, ∀s ∈ S (13) f dk ≥ 0, ∀d ∈ D, ∀k ∈ K d (14)
2) Maximizing the Minimum Allocated Volume: Following the same reasoning, MM-SPP is obtained by replacing the capacity constraint (6) in LP 2 by constraint (9) in LP 3.

IV. APPROXIMATION ALGORITHMS

Solving the linear programs presented in the previous section is not viable in practice. Particularly, when considering large topologies with a large number of demands, these linear programs can become very difficult to solve and solutions will heavily depend on the solver package. In this work, we develop approximation algorithms based on a primal-dual approach. This approach uses a basic property of the duality theory in linear programming: considering a maximization problem, the objective value of any feasible solution to the primal problem in is at most the objective value of any feasible solution of its dual. Therefore, by comparing the objective values of the primal and dual formulations, we can measure the closeness of a solution (for the primal problem) to the optimal one. By this, we obtain ρ-approximations to the problem: for a maximization problem, a ρ-approximation is an algorithm that computes a solution with an objective value A(I) verifying A(I) ≥ ρOPT(I), where OPT(I) is the optimal objective value and ρ a real number from the interval [0, 1]. Sometimes ρ is given in the form ρ = 1 -. Note that, there has been considerable work on approximation for multicommodity problems: the paper in [START_REF] Fleischer | Approximating fractional multicommodity flow independent of the number of commodities[END_REF] presents an excellent overview over the work. Particularly, our work will be mainly based on the algorithms and analysis in [START_REF] Garg | Faster and simpler algorithms for multicommodity flow and other fractional packing problems[END_REF].

A. MS-DPP

In order to adapt the primal-dual approach for MS-DPP, we introduce in LP 5 the dual problem corresponding to LP 1. In this dual problem, ω e denotes the dual variables associated with constraint (2) in LP 1. With some intuition, let us consider that ω e is a weight associated with link e. ω e represents also the marginal cost of using an additional unit of bandwidth form the link capacity. Similarly, we suppose that the weight of one cycle is the sum of the weights for its component links. Then, constraint (16) says that the weight for each cycle associated with demand d is at least 1. This observation will contribute in formulating the approximation for MS-DPP. Subject to:

e∈E α edk ω e ≥ 1, ∀d ∈ D, ∀k ∈ K d ( 16
)

ω e ≥ 0, ∀e ∈ E (17)
Algorithm 1 computes a ρ-approximation to the MS-DPP problem. The algorithm starts by assigning a weight ω e = δ for each link in the network (δ is chosen depending on and is defined later in Theorem 1). Then, we define in (18) the set K * of cycles with weight less than 1. The algorithm loops until K * becomes empty.

K * = {k ∈ K d , ∀d ∈ D/ω k = e∈E α edk ω e < 1} (18)
At each iteration, the algorithm selects the shortest cycle k * in K * (let us say k * realizes demand d i.e. k * ∈ K d ) with respect to weights ω e , and increases both the primal and the dual variables associated with this cycle: for the primal problem, the algorithm augments flow along this cycle. Note that shortest cycle computation is done using the algorithm introduced in [START_REF] Suurballe | A quick method for finding shortest pairs of disjoint paths[END_REF]. The amount of flow sent along cycle k * is determined by the bottleneck capacity of the cycle, using the original capacities. The bottleneck capacity of a cycle is the capacity of the minimum capacity link in the primary and the backup paths. If we denote this capacity by c. The primal solution is updated by setting f dk * = f dk * +c (this solution can be scaled to become feasible). Then, the dual variables are updated so that the weight of a link is exponential in the congestion of the link. The update function for each link e on k * is defined as ω e = ω e (1 + c Ce ). This update ensures that the weight of the bottleneck link on k * increases by a factor of (1 + ) (the dual solution can also be scaled to become feasible). Thus, at the end of every iteration we have implicit primal and dual feasible solutions. The algorithm terminates when all paths have a weight that is greater or equal to 1, i.e. K * is empty. Note that, the final solution may be infeasible since we are using the original capacities. Thus, the total allocated flow f t = d∈D k∈K d f dk is scaled according to Lemma 1 and yields a feasible solution to the MS-DPP problem. Moreover, the approximation guarantee and the corresponding running time of Algorithm 1 are given in Theorem 1.

Algorithm 1 Approximation Algorithm for MS-DPP

1: t = 0; ω e = δ, ∀e ∈ E 2: while K * , given by (18), is not empty do Full proofs for the above lemma and theorem are reported in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF] and are omitted in this work due to page limitations.

B. MM-DPP

As we proceeded for the MS-DPP, we formulate the dual of LP 2 in LP 6. In this dual problem, π d denotes the dual variables associated with constraint [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF] and ω e the dual variables associated with constraint (6) in LP 2. Constraint (21) says that π d is the minimum weight for the cycles associated with demand d. Technically, the primal-dual algorithm, presented in Algorithm 2 starts by assigning a weight of δ Ce to link e. The algorithm alternates between primal flow variables and dual weight variables to satisfy the capacity constraint in [START_REF] Hauser | Capacity design of fast path restorable optical networks[END_REF] and the weight constraint in (21). Particularly, the algorithm proceeds in phases. In each phase and for each demand d, the Subject to:

d∈D π d ≥ 1 (20) e∈E α edk ω e ≥ π d , ∀d ∈ D, ∀k ∈ K d (21
)

ω e ≥ 0, ∀e ∈ E (22)
shortest cycle k * ∈ K d is calculated using the last values of weights ω e . Shortest cycle computation is also done using the algorithm introduced in [START_REF] Suurballe | A quick method for finding shortest pairs of disjoint paths[END_REF]. The algorithm allocates 1 unit of flow between source and destination. Once the flow is sent, the weight of the links that carry the flow is increased, based on an exponential function. Therefore, the algorithm alternates between sending flow along shortest cycle and adjusting the weight of the links along which flow has been sent until the optimal solution is reached. The entire procedure ends as soon as Ω > 1, where Ω denotes the objective of the dual problem LP 6. Finally, Theorem 2 states the polynomial performance of the above algorithm. Note that, at the end of the iterations, the allocated flow is infeasible for the primal problem and thus need to be scaled down according to Lemma 2.

t = t + 1 9: end while Lemma 2 At the end of Algorithm 2, F = t-1 log 1+ ( 1 δ ) . Theorem 2 Assuming that = 1 -ρ 1 3 and δ = ( E 1-) -1/ , Algorithm 2 computes a ρ-approximation to MM-DPP in time O 2D log D 1 log 1+ E 1-
T mwc , where T mwc is the time required to compute a minimum weight cycle.

Full proofs and additional remarks for the above lemma and theorem are reported in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF] and are omitted in this work due to page limitations.

C. Sharing Backup Bandwidth: MS-SPP and MM-SPP

When backup bandwidth is shared, the results obtained for the dedicated case could not be directly extended. Let us first present the approximation algorithm for MM-SPP. In order to formulate the corresponding approximation, we introduce the dual problem in LP 7 where ω es denotes the dual variable associated with constraint (13). With some care while extending the results, the same analysis can be carried for this problem. The approximation, presented in Algorithm 3 follows the same sketch as for the dedicated protection case. It alternates between allocating flows to shortest cycles and updating the weights of the links on these cycles. However, two main differences are worth to be mentioned.

1) The shortest cycle computation in step 4 requires additional attention. Considering that ω es is a weight associated with link e in situation s, the weight of one cycle is expressed as the sum of two components: a first component that adds up the weights for the links in the primary path, whenever this path is available, and a second component that adds up the weights for the links in the backup path, whenever the corresponding primary path is failing. Then, finding a shortest cycle with respect to the above mentioned weighting is not an easy task: a detailed review of the field is provided in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF]. Thus, in order to remedy to this problem, we use a brute-force approach that assumes that the sets of cycles for all demands are precomputed. Particularly, this cycle set (of exponential size) can be reduced by limiting the hop number, following, for instance, some quality of service constraints. Then, the shortest cycle that minimizes (25) is found by simple comparison over the computed set. Note that the cycle set computation time is not accounted in our algorithm.

2) The weight update is done as in the following: the weight, ω es , corresponding to link e in situation s, is updated if e belongs to the primary path (resp. the backup path) of the shortest cycle, and the primary path is available (resp. failing) in situation s.

Lemma 3 At the end of Algorithm 3,

F = t-1 log 1+ ( 1 δ ) .
Theorem 3 Assuming that = 1-ρ

1 3 and δ = ( E(E+1) 1- ) -1/ , Algorithm 3 computes a ρ-approximation to the MM-SPP in time O 2D log D 1 log 1+ E(E+1) 1-
T mwc , where T mwc is the time required to compute a shortest cycle.

In Lemma 3, we report the scaling that yields a feasible primal solution, and in Theorem 3, we report the performance of Algorithm 3. In Theorem 3, the time required to compute a minimum weight cycle is dominated by a linear search procedure on the precomputed set of cycles. Let us denote K the maximum number of cycles realizing a demand d ∈ D, i.e. K = max d∈D K d . Then the linear search procedure that computes the minimum weight cycle runs in O(K) and the global running time of Algorithm 3 is

O 2D log D 1 log 1+ E(E+1) 1-
K . The same observations apply to the MS-SPP problem, and an extended presentation is provided in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF]. Moreover, in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF],

we introduce an efficient procedure that enables to tackle the computational complexity of the linear search procedure. end for 13: t = t + 1 14: end while

V. RELATED WORK

Flow allocation with path protection mechanisms has been investigated in a number of recent papers. Particularly, three relevant papers [START_REF] Hauser | Capacity design of fast path restorable optical networks[END_REF], [START_REF] Fleischer | A scalable algorithm for the minimum expected cost restorable flow problem[END_REF] and [START_REF] Todimala | Approximation algorithms for survivable multicommodity flow problems with applications to network design[END_REF] are similar to our work. First, in [START_REF] Hauser | Capacity design of fast path restorable optical networks[END_REF], the authors introduce algorithms for capacity dimensioning for optical networks. The objective is to size the demand volume in order to satisfy the capacity constraints. The authors use a path protection mechanism. However, sharing is only enabled between the flows realizing the same demand. Based on a maximum concurrent flow formulation, they provide a ρapproximation algorithm that runs in time polynomial in the problem size. Second, in [START_REF] Fleischer | A scalable algorithm for the minimum expected cost restorable flow problem[END_REF], the authors introduce a model for the computation of a minimum cost multicommodity flow with a path protection mechanism. Full sharing is supported but the primary flows are allocated on a set of disjoint paths that are precomputed for each demand. The authors provide a ρapproximation algorithm and the running time depends on the number of disjoint paths. Third, [START_REF] Todimala | Approximation algorithms for survivable multicommodity flow problems with applications to network design[END_REF] investigated very recently the problem of survivable flow allocation with full sharing between the demands. A preliminary step computes the se of failure disjoint paths and feed the approximation algorithm (note that the corresponding problem for the precomputation step is N P-hard). The authors provide a ρ/2-approximation algorithm with the running time depending on the number disjoint pair of paths in the network. They suggest reducing the running time by reducing the precomputed set of paths. A broader view of the state of the art, that also cover general approximations for multicommodity flow problems is presented in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF].

VI. NUMERICAL RESULTS

To illustrate the performance of our algorithms, we performed a series of experiments over simulation topologies. We consider complete graph topologies. In graph theory, a complete graph is a simple graph where an link connects every pair of vertices. Certainly, complete graphs were not chosen for simulation as realistic topologies. Nevertheless, as complete graphs are maximally connected (i.e. the only vertex cut which disconnects the graph is the complete set of vertices or roughly saying, they have many alternate paths), they will illustrate the extreme performance points in our experiments. In all our simulations, each link is assumed to have a capacity of 100 units and demands are considered between all the nodes in the graph. Figure 1 illustrates the compared performance for the different algorithms presented in section IV. It expresses the total allocated volume for each algorithm as a function of the node number of the complete graph. Note that, results concerning provisioning for non protected flows are included for reference, although not directly introduced in this paper. These are annotated MS-NP and MM-NP for the solution that maximizes the sum of the allocated flows and the minimum allocated demand respectively, both with no protection requirements. Figure 1 shows that the gap between the total allocated volume for MS-DPP and for MS-SPP is very large: around 1800 bandwidth units for the 9-node topology. This is not the case when we compare the allocation for MM-DPP and MM-SPP. Intuitively, this is due to the fact that sharing becomes less efficient when the objective is to guarantee some fairness between demands (as for MM problems). However, we note that for the two couples of problems, the gap keeps on increasing when the number of nodes increases. This is a normal result of large highly-connected topologies that offer more paths for allocation and thus more possibilities to share backup flows. Finally, the no-protection problems achieve, as expected, the highest allocated volume at the expense of high vulnerability to network failures.

VII. CONCLUSION

In this work, we provide ρ-approximations for flow allocation problems with end-to-end protection. While a large number of papers have provided efficient solutions to similar problems, this paper concentrates on guaranteed approximations. Moreover, the originality is increased by comparing for the first time two different approaches for network provisioning and evaluating the impact of fairness. Therefore, future work will concentrate on providing an extension to the max-min fair problems that enable to approximate the global optimal solution. Moreover, we will study, in a similar work, algorithms for flow allocation problems with local protection. An extended version of this work is provided in [START_REF] Lahoud | Survivable routing and flow allocation in next generation internet networks[END_REF] containing additional simulation results and numerical evaluation as well as the full mathematical proofs. Moreover, in a recent work, we provide efficient methods that tackle the computational complexity of the shared path protection versions.

LP 5

 5 MS-DPP: Dual problem Minimize e∈E C e ω e (15)

3 : 5 : 1 Theorem 1 1 2

 35111 Let k * ∈ K d be the shortest cycle in K * 4: c = min{C e : ∀e ∈ k * } f dk * = f dk * + c and ω e = ω e (1 + c Ce ), ∀e ∈ k * At the end of Algorithm 1, the total allocated flow f t = d∈D k∈K d f dk need to be scaled by log 1+ ( 1+ δ ) in order to become feasible. Assuming that = 1ρ and δ = (1 + )((1 + )E) -1/ , Algorithm 1 computes a ρ-approximation to MS-DPP in time O(EDT mwc log 1+ 1+ δ ) where T mwc is the time required to compute a shortest cycle.

LP 6

 6 MM-DPP: dual problem Minimize Ω = e∈E C e ω e (19)

Algorithm 2 3 : 4 :

 234 Approximation algorithm for MM-DPP 1: t = 0; ω e = δ Ce , ∀e ∈ E 2: while Ω < 1 do for d = 1, . . . , D do Let k * be the shortest cycle in K d 5:f dk * = f dk * + 1 6:f e = f e + 1 and ω e = ω e (1 + Ce ), ∀e ∈ k *

Algorithm 3 5 : 6 :f

 356 α p edk + θdks α b edk )ω es ≥ π d , ∀d ∈ D, ∀k ∈ K d (25) ω es ≥ 0, ∀e ∈ E, ∀s ∈ S (26) Approximation algorithm for MM-SPP 1: t = 0; ω es = δ Ce , ∀e ∈ E∀s ∈ S 2: while Ω < 1 do 3: for d = 1, . . . , D do 4: Let k * = (p * , b * ) be the shortest cycle in K d for s = 1, . . . , S do if θ dk * s = 1 then 7: f es = f es + 1 and ω es = ω es (1 + Ce ), ∀e ∈ p * es = f es + 1 and ω es = ω es (1 + Ce ), ∀e ∈ b *

Fig. 1 .

 1 Fig. 1. Comparison of bandwidth consumption