# faster_and_better_simple_temporal_problems__370faac6.pdf Faster and Better Simple Temporal Problems Dario Ostuni1, Alice Raffaele2, Romeo Rizzi1, Matteo Zavatteri1* 1University of Verona, Department of Computer Science, Strada Le Grazie 15, 37134 Verona (Italy) 2University of Trento, Department of Mathematics, Via Sommarive 14, 38123 Povo (Italy) {dario.ostuni, romeo.rizzi, matteo.zavatteri}@univr.it, alice.raffaele@unitn.it In this paper we give a structural characterization and extend the tractability frontier of the Simple Temporal Problem (STP) by defining the class of the Extended Simple Temporal Problem (ESTP), which augments STP with strict inequalities and monotone Boolean formulae on inequations (i.e., formulae involving the operations of conjunction, disjunction and parenthesization). A polynomial-time algorithm is provided to solve ESTP, faster than previous state-of-the-art algorithms for other extensions of STP that had been considered in the literature, all encompassed by ESTP. We show the practical competitiveness of our approach through a proof-ofconcept implementation and an experimental evaluation involving also state-of-the-art SMT solvers. Introduction and Related Work The Temporal Constraint Satisfaction Problem (TCSP), originally introduced by (Dechter, Meiri, and Pearl 1991), takes as input a finite set of real variables and a finite set of constraints. Two kinds of constraints are allowed: unary and binary; both can take a disjunctive form. A unary constraint has the form x [ℓ1, u1] [ℓn, un], where x is a variable and ℓi, ui R { , + }, ℓi ui . A binary constraint has the form y x [ℓ1, u1] [ℓn, un], where x and y are variables and, again, ℓi, ui R { , + }, ℓi ui . Regardless of the type of constraint, the corresponding involved intervals are disjoint. Note that each unary constraint x [ℓ1, u1] [ℓn, un] can be seen as a binary one x z [ℓ1, u1] [ℓn, un] where z is an extra variable on which we impose the unary constraint z [0, 0]. As such, one single unary constraint suffices. Or, we can even relax that one and then consider the solution obtained by subtracting the value of z from that of every other variable. Indeed, the solution space of a TCSP without unary constraints is closed under rigid shifting. We remark that binary constraints are disjunctions over the same pair of variables (this restriction is overcome in (Stergiou and Koubarakis 2000) with the proposal of disjunctive temporal networks). TCSP asks the following question: does there exist an assignment of real values to the variables such that all constraints are *Corresponding author Copyright 2021, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. satisfied? TCSP is NP-complete (Dechter, Meiri, and Pearl 1991). The Simple Temporal Problem (STP) is the fragment of TCSP whose set of constraints consists of atoms of the form y x [ℓ, u] only. Historically, STP allows for two representations: the interval based one (as we just discussed above) or a set of inequalities y x k where x, y are variables and k R. While these are equivalent (y x k can be written as y x [ , k]), the second representation is more elementary as y x [ℓ, u] amounts to (y x u) (x y ℓ). STP is in P (Dechter, Meiri, and Pearl 1991). The set of constraints of an STP can also be generalized to include strict inequalities y x < k and inequations y x = k. Of course, any strict inequality y x < k can be seen as a non-strict inequality y x k plus the inequation y x = k. Inequations are useful to model temporal plans in which, for example, we require two events not to happen at the same time. Koubarakis augmented STP with disjunctions on inequations (y1 x1 = k1) (yn xn = kn) in (Koubarakis 1992). He proved tractability of this extension by providing an algorithm that runs in O(||C||4), where C is the set of constraints and ||C|| is the number of atoms y x k, { , =} appearing in C. As far as we know, this was still the bound for this problem. Gerevini and Cristani defined STP =, which is a restriction of (Koubarakis 1992) allowing only simple inequations and not disjunctions of these, resulting in the possibility of handling both sets of strict-inequalities and inequations (Gerevini and Cristani 1997). They provided an algorithm to solve STP = that runs in O(n3 + h), where n is the number of variables and h is the number of inequations (or O(n3) if there are only strict and non-strict inequalities). As far as we know, the result in (Gerevini and Cristani 1997) was the state of the art for STP =, still used by more recent works (e.g., (Broxvall 2002; Montanari et al. 2012; Cooper, Maris, and R egnier 2013; Carbonnel and Cooper 2015)). For more details about temporal reasoning, the interested reader is referred to (Vila 1994; Schwalb and Vila 1998; Bartak, Morris, and Venable 2014). Satisfiability Modulo Theory (SMT) (Barrett et al. 2009) can address generalizations of the problems mentioned above by relying on the quantifier-free fragment of the theory of real difference logic (QF RDL). QF RDL allows for The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI-21) arbitrary Boolean combinations of atoms y x k, where x, y are real variables, {<, , >, , =, =}, and k Q. In this logic, strict inequalities y x < k are usually turned into non-strict inequalities y x k ε, with ε treated either numerically (Armando et al. 2005) or symbolically as an infinitesimal parameter (Dutertre and de Moura 2006). As far as we know, the latter is the state of the art on difference arithmetic constraints (Dutertre and de Moura 2006; de Moura, Dutertre, and Shankar 2007). Note that the core algorithms to solve the problems mentioned above are typically based on tuned versions of shortest path algorithms or the simplex method, e.g., (Dutertre 2014). It is thus interesting and reasonable, e.g., when developing a more efficient procedure to solve STP with strict inequalities, to also make a comparison with SMT solvers supporting QF RDL. Organization and Contribution We start by giving background on STP. Then, we define the Extended Simple Temporal Problem (ESTP), in which we allow for inequalities, strict inequalities and monotone Boolean formulae on inequations. We give a characterization of ESTP. Specifically, we define verification criteria to detect inconsistency or decide consistency of any instance of ESTP. These allow us to provide a strongly polynomialtime algorithm to solve ESTP, which is faster than current state-of-the-art algorithms for previously studied extended classes of STP. We discuss a proof-of-concept implementation by comparing several variants of shortest paths algorithms. Moreover, we encode our model as a QF RDL formula since it is well-known that the satisfiability of conjunctions of atoms y x k for { , <} is tractable. We evaluate our performance against the state-of-the-art SMT solvers that competed in the 15th International Satisfiability Modulo Theories Competition SMT-COMP 2020 for QF RDL (Model Validation Track and Single Query Track)1. Computational results confirm the practical competitiveness of our approach, which can solve instances close to 3 million variables within 100 seconds. Finally, we draw conclusions and discuss future work. Background In this section we sum up essential information on STP and how to efficiently solve it through a reduction to the Single Source Shortest Paths problem (SSSP) (Cormen et al. 2009). Problem 1 (STP). Given a finite set X of real variables, and a finite set C of inequalities of the form y x k with y, x X and k R, does there exist a mapping δ: X 7 R satisfying all constraints in C? An instance of STP is consistent if such a solution δ exists; inconsistent otherwise. We assume that any instance of STP appearing in this paper has no dominated inequalities, where an inequality y x k dominates an inequality y x k if k < k . 1https://smt-comp.github.io/2020/index.html Example 1. Let S = (X, C) be the following instance of STP: X := {x1, x2, x3, x4, x5, x6, x7}, C := {x2 x1 2.2, x3 x2 3.5, x1 x3 5.7, x4 x5 2, x5 x7 1, x7 x6 6, x6 x4 9, x6 x3 3.3, x2 x4 2}. Most of the algorithms that solve instances of STP rely on their corresponding directed weighted graph representation. Definition 1 (Directed weighted graph). A directed graph is a pair (V, A) where V is a set of nodes and A V V is a set of arcs (or, equivalently, directed edges). A directed weighted graph is a triple (V, A, w) where (V, A) is a directed graph and w: A 7 R is a weight function assigning a real value to each arc. We write Px,y := (x, x1), . . . , (xn, y) for the path (sequence of arcs) going from x to y through a sequence of distinct nodes. A cycle is a path Px,y where x = y. In case of directed weighted graphs, we write w(Px,y) for the weight of the path (i.e., the sum of the weights of the arcs in the sequence). A path or a cycle Px,y in a weighted graph is negative if w(Px,y) < 0. Definition 2 (Constraint graph). Let S = (X, C) be an instance of STP. The corresponding constraint graph of S is the directed weighted graph GS = (X, A, w) where: A := {(x, y) | y x k C}, and w(x, y) := k for each y x k C. Figure 1 shows the constraint graph of Example 1. Theorem 1 ((Dechter, Meiri, and Pearl 1991)). An instance of STP is consistent iff GS has no negative-weight cycle. Deciding whether an instance of STP S = (X, C) is consistent can be done by computing a potential function for GS, i.e., a function π: X 7 R such that π(y) π(x) w(x, y) for each (x, y) A. This feasible potential is a possible solution δ and can be computed by a run of any SSSP algorithm. Since we deal with temporal problems, when unary constraints are not involved, it is also reasonable to seek a non-negative π; a guarantee that, unfortunately, we do not get by just computing a feasible potential. However, this is not an issue because potential functions are shift-invariant (Cormen et al. 2009). That is, for any feasible potential function π and any σ R, it holds that the function defined as π (x) := π(x)+σ for each x X is still a feasible potential function. Indeed, for any (x, y) A: π(y) π(x) w(x, y) π(y) π(x) + σ w(x, y) + σ (for any σ R) (π(y) + σ) (π(x) + σ) w(x, y) π (y) π (x) w(x, y). Example 1 is consistent. Indeed, a potential function π for its constraint graph is shown in Figure 1. Thus, a solution is δ(x1) := π(x1) = 0, δ(x2) := π(x2) = 2.2, δ(x3) := π(x3) = 5.7, δ(x4) := π(x4) = 0, δ(x5) := π(x5) = 2, δ(x6) := π(x6) = 9, and δ(x7) : π(x7) = 3. In case we desire δ to be non-negative, we define δ(x) := π(x) + σ for each x X, where σ := | minx X π(x)| = 9. Figure 1: Constraint graph of Example 1 (ignoring arc colors) and Example 2 (considering red arcs too). Near the nodes, there are two labels, π/π + 9: π (in gray) is the value of the feasible potential taking x1 as a source, whereas π +9 (in green) is the corresponding rigidly shifted value. We do not draw formulae on inequations to keep the figure clear. Extended Simple Temporal Problem In (Koubarakis 1992), STP was extended to also handle disjunctions on inequations. The definition of Extended STP (ESTP) generalizes (Koubarakis 1992) by allowing arbitrary monotone Boolean formulae on inequations, rather than only disjunctions. Problem 2 (ESTP). Given a finite set X of real variables, a finite set C of inequalities of the form y x k with y, x X and k R, a finite set C< of strict inequalities of the form y x < k with y, x X and k R, and a finite set C = of monotone Boolean formulae on inequations generated by the grammar F ::= y x = k | F F | F F | (F) with y, x X and k R, does there exist a mapping δ: X 7 R satisfying all constraints in C , C< and C =? Similarly to STP, an instance of ESTP is consistent if such a solution δ exists; inconsistent otherwise. Let S = (X, C , C<, C =) be any instance of ESTP. We write y x k for a generic atom appearing in some constraint, where { , <, =}. We denote by AS the set of all atoms appearing in S and, similarly, we denote by AF := {y x = k | y x = k F} AS the set of atoms of any F C =. Moreover, we just write inequality when we do not care if it is strict or not, and we still assume that any instance of ESTP appearing in this paper has no dominated inequalities, where, this time, an inequality y x k dominates an inequality y x k if either k < k , or is < and is and k = k . Example 2. Let S = (X, C , C<, C =) be the following instance of ESTP: X := {x1, x2, x3, x4, x5, x6, x7}, C := {x2 x1 2.2, x3 x2 3.5, x1 x3 5.7, x4 x5 2, x5 x7 1, x7 x6 6, x6 x4 9} C< := {x6 x3 < 3.3, x2 x4 < 2} C = := {x6 x1 = 9 (x4 x7 = 3 x6 x5 = 7.14)}. One could fairly wonder whether C and C = together subsume C<. It is true; indeed, any strict inequality of the form y x < k can be rewritten as a classic inequality y x k plus an inequation y x = k. The reason we also support strict inequalities is because we want to explore their structure without masquerading them as the composition of different parts. We now discuss three independent conditions to identify inconsistent instances of ESTP. It will later turn out that any instance of ESTP not affected by any of these conditions is consistent. The notion of relaxation of an ESTP instance helps to state these conditions. Definition 3 (Relaxation of an ESTP instance). Let S = (X, C , C<, C =) be an instance of ESTP. The relaxation of S is the following instance of STP R = (XR, CR), where CR := C {y x k | y x < k C<}. In other words, the relaxation of S keeps all non-strict inequalities and turns each strict inequality into a non-strict inequality. Note that, by construction, R cannot have dominated inequalities either. The relaxation of the instance in Example 2 is R = (XR, CR), where XR is the same of Example 2 and CR is exactly the set C of Example 1. Lemma 1. Let S be an instance of ESTP and let GR be the constraint graph of its relaxation. If GR has a negativeweight cycle, then S is inconsistent. Proof. A solution for S would also be a solution for R. This cannot exist if GR has a negative-weight cycle (by Theorem 1). Figure 1 does not contain any negative-weight cycle. Definition 4 (Arc color). Let S = (X, C , C<, C =) be an instance of ESTP and GR = (X, A, w) be the constraint graph of its relaxation. We say that an arc (x, y) in GR is red if S contains the strict inequality y x < w(x, y). A path Px,y is red if it contains a red arc. That is, given an instance of ESTP S, the red arcs in the constraint graph of its relaxation GR identify exactly strict inequalities of S. In Figure 1, (x3, x6) and (x4, x2) are red since {x6 x3 < 3.3, x2 x4 < 2} C< in Example 2. Red arcs allow for the definition of a condition to discover other inconsistent instances of ESTP. To the best of our knowledge, this condition has never been identified before. Lemma 2. Let S be an instance of ESTP and let GR be the constraint graph of its relaxation. If GR has a zero-weight cycle containing a red arc, then S is inconsistent. Proof. Assume that S admits a solution δ and let c := (x1, x2), . . . , (xe, xe+1 = x1) be a zero-weight cycle in GR where (x1, x2) is a red arc. Then δ(x2) δ(x1) < w(x1, x2) and δ(xi+1) δ(xi) w(xi, xi+1), for every i = 2, . . . , e. Summing up these inequalities (one for every arc in c), the valuations of δ on the e nodes simplify away and we end up with the contradiction 0 < 0. Figure 1 contains two zero-weight cycles: c1 := (x1, x2), (x2, x3), (x3, x1) and c2 := (x4, x6), (x6, x7), (x7, x5), (x5, x4) . Anyway, none of them contains red arcs. We now provide the third (and last) condition to identify inconsistent instances of ESTP. Definition 5 (Hopeless formula). Let S = (X, C , C<, C =) be an instance of ESTP and GR be the constraint graph of its relaxation. A monotone formula F C = is said hopeless if F is false under any Boolean evaluation that assigns false to all y x = k AF for which GR contains the two non-red weighted paths w(Px,y) = k and w(Py,x) = k. Lemma 3. Let S be an instance of ESTP. If S has a hopeless formula, then S is inconsistent. Proof. Let S = (X, C , C<, C =) be an instance of ESTP and F be a hopeless formula. Let A F be the set of atoms y x = k of F for which GR contains the two non-red weighted paths w(Px,y) = k and w(Py,x) = k. Suppose that S is consistent and let δ be a solution for it. Then, δ must satisfy F. However, for each atom in A F we have that δ(y) δ(x) = k because both δ(y) δ(x) k and δ(x) δ(y) k hold. Therefore, none of these atoms can be satisfied by δ. But then, by definition of hopeless, δ does not satisfy F either because, even if δ satisfies all remaining atoms and that is exactly why this check can be done in polynomial time F is still false under such an interpretation (contradiction). Consider the unique formula on inequations in Example 2: x4 x7 = 3 is the unique atom for which Figure 1 contains the two non-red weighted paths w( (x7, x5), (x5, x4) ) = 3 and w( (x4, x6), (x6, x7) ) = 3. Thus, any possible solution δ (if any exists) will not satisfy that atom. Anyway, that formula is not hopeless since its remaining atoms could still make it true. To sum up, an inconsistency certificate for an instance S of ESTP is either a negative-weight cycle in GR or a zeroweight cycle containing a red arc in GR or a hopeless formula in S. We are finally in position to define consistency. Theorem 2. An ESTP instance is consistent iff none of the conditions of Lemma 1, Lemma 2 and Lemma 3 applies. Proof. Let S = (X, C , C<, C =) be an instance of ESTP. ( ) If S is consistent, then none of the conditions of Lemma 1, Lemma 2 and Lemma 3 applies. In fact, if any did, S would be inconsistent. ( ) If none of the conditions of Lemma 1, Lemma 2 and Lemma 3 applies, then S is consistent. To prove it, we build a mapping δ: X 7 R as follows: 1. Let π be a feasible potential for the constraint graph GR of the relaxation of S. 2. Let G R := (X, A, w ) be the reweighted graph obtained from GR where w (x, y) := w(x, y) + π(x) π(y) for each (x, y) A. 3. Let A0 := {(x, y) | (x, y) A, w (x, y) = 0} be the subset of zero-weight arcs of G R and let D0 := (X, A0) be the corresponding directed acyclic graph (DAG). Note that a cycle in D0 is a zero-weight cycle in both GR and G R, since the reweighting operation maintains shortestpaths and cycle weights. 4. Let P := {X1, . . . , X|P|} be the partition of X coinciding with the set of strongly connected components (SCCs) of D0. Note that each SCC is a rigid component. That is, a set of nodes such that, once the value of one of these nodes is fixed, so are the values of all the other nodes in the same component. 5. Let DP := (P, AP) be the DAG of the SCCs of D where AP := {(Xi, Xj) | Xi, Xj P, Xi = Xj, (x, y) A0, x Xi, y Xj}. 6. Let ε := 1, min y x k AS, |k+π(x) π(y)|>0 |k + π(x) π(y)| 7. Let T := X1, . . . , X|P| be any topological sort of DP. 8. Define δ as follows: δ(x) := π(x) + 0ε for each x X|P| δ(x) := π(x) + 1ε for each x X|P| 1 . . . . . . δ(x) := π(x) + (|P| 1)ε for each x X1. We claim that δ is a solution for S. Note that we do not need to check atomic constraints involving variables in the same SCC. Indeed, for each y x k AS with x, y in the i-th SCC, by letting εi := (|P| i)ε, it holds that: π(y) π(x) k π(y) π(x) + εi k + εi (π(y) + εi) (π(x) + εi) k δ(y) δ(x) k. Notice that, due to Lemma 1 and Lemma 2, if is or <, then the atom always holds. Instead, if is =, then the atom might also not be satisfied; in such a case it must belong to some formula F which has some other atom satisfied (otherwise Lemma 3 would have applied). Therefore, what we are really left to prove is that any atom y x k AS, with y and x belonging to two different SCCs, is satisfied by δ. Let Xi and Xj be two different SCCs with i < j in the topological sort T. Let εi := (|P| i)ε and εj := (|P| j)ε be the distances of δ from π for each x Xi and for each y Xj, respectively. For each type of atom (i.e., for each ), we consider its two possible orientations: the right one from Xi to Xj and the left one from Xj to Xi. We rely on the fact that εj < εi, since i < j. We start by considering the right oriented atoms, i.e., those of the form y x k. Case y x k. We highlight that π(y) π(x) k holds. If we substitute δ(y) π(y) for εj and δ(x) π(x) for εi, we obtain δ(y) π(y) < δ(x) π(x) and thus δ(y) δ(x) < π(y) π(x) k. Case y x < k. Same of Case y x k. Case y x = k. We have two cases: If π(y) π(x) = k, then, by substituting δ(y) π(y) for εj and δ(x) π(x) for εi, we obtain δ(y) π(y) < δ(x) π(x), implying δ(y) δ(x) < π(y) π(x) = k. 0/0.02/9.02 2.2/ 2.18/6.82 5.7/ 5.68/3.32 3/ 3/6 (+0ε) (+1ε) Figure 2: Graphical construction of the solution δ for the instance in Example 2. Node labels have the form π/δ/δ+9, where π (in gray) is the feasible potential, δ (in black) is the solution and δ + 9 (in green) is the rigidly shifted value. Otherwise π(y) π(x) = k; since |k+π(x) π(y)| > 0 and εj εi < 0, it holds that εj εi < |k+π(x) π(y)|. By substituting δ(y) π(y) for εj and δ(x) π(x) for εi, we get δ(y) π(y) δ(x)+π(x) < |k+π(x) π(y)|. By solving the modulus, we get that: If k + π(x) π(y) > 0, then δ(y) δ(x) < k. Otherwise k + π(x) π(y) < 0, and then δ(y) δ(x) < k + 2(π(y) π(x)) = k. Then, we consider the left oriented atoms, i.e., x y k. Case x y k. We highlight that π(x) π(y) < k. In fact, if π(x) π(y) were equal to k, there would exist a zero-weight arc (y, x) in the reweighted graph G R and therefore an arc (Xj, Xi) in the DAG of the SCCs DP, contradicting the topological sort T. Since k + π(y) π(x) > 0 and εj εi < 0, it holds that εj εi < k + π(y) π(x). By substituting δ(x) π(x) for εi and δ(y) π(y) for εj, we get δ(x) π(x) δ(y)+π(y) < k+π(y) π(x) which implies δ(x) δ(y) < k. Case x y < k. Same of Case x y k (once again π(x) π(y) = k cannot hold, otherwise the topological sort T would be contradicted). Case x y = k. We have two cases: If π(x) π(y) = k, then by substituting δ(x) π(x) for εi and δ(y) π(y) for εj, we obtain δ(y) π(y) < δ(x) π(x) implying δ(x) δ(y) > π(x) π(y) = k. Otherwise π(x) π(y) = k; since |k+π(y) π(x)| > 0 and εj εi < 0, it holds that εj εi < |k+π(y) π(x)|. By substituting δ(y) π(y) for εi and δ(x) π(x) for εj we get δ(y) π(y) δ(x)+π(x) < |k+π(y) π(x)|. By solving the modulus, we get that: If k + π(y) π(x) > 0, then δ(y) δ(x) < k + 2(π(y) π(x)) and thus δ(x) δ(y) > k+2(π(x) π(y)) = k. Otherwise k π(y) + π(x) < 0, then δ(y) δ(x) < k and thus δ(x) δ(y) > k. Algorithm 1: ESTP solver Input: An instance S = (X, C , C<, C =) of ESTP. Output: A solution δ if S is consistent; inconsistent otherwise. 1 if Lemma 1 applies then return inconsistent; 2 if Lemma 2 applies then return inconsistent; 3 if Lemma 3 applies then return inconsistent; 4 Compute δ as discussed in the proof of Theorem 2; 5 return δ; Our ESTP solver is summarized in Algorithm 1. For the instance S in Example 2, Figure 1 shows a feasible potential π for its relaxation. Figure 2 represents the reweighted graph of that in Figure 1 (considering all appearing arcs). The same Figure also shows the remaining DAGs (ignoring all weights). Specifically, D0 is the DAG consisting of all snake-pattern edges (with its SCCs highlighted in gray), whereas DP is the DAG having as nodes the sets X1 := {x1, x2, x3} and X2 := {x4, x5, x6, x7} and as unique arc the snake-pattern red one. We consider the topological sort T := X1, X2 . Regarding all atoms of S, the smallest |k + π(x) π(y)| > 0 is due to the atom x6 x5 = 7.14 in the formula on inequations and its value is 0.14. Therefore, ε := 0.02. We compute the mapping δ as follows: we set δ(x) := π(x) + 0ε for each x X2 and we set δ(x) := π(x) + 1ε for each x X1. The reader can check that δ(x1) := π(x1) + 1ε = 0.02, δ(x2) := π(x2) + 1ε = 2.18, δ(x3) := π(x3) + 1ε = 5.68, δ(x4) := π(x4) + 0ε = 0, δ(x5) := π(x5) + 0ε = 2, δ(x6) := π(x6)+0ε = 9, and δ(x7) := π(x7)+0ε = 3 is a solution. In case, δ can be rigidly shifted by 9 to make it non-negative. Theorem 3. Let S = (X, C , C<, C =) be an instance of ESTP. Let n := |X|, m := |C | + |C<| and h := P F C = |AF |. Then, Algorithm 1 runs in time O(nm + h). Proof. We analyze the steps needed by Algorithm 1. It takes O(nm) to compute a feasible potential of GR or prove that none exists (i.e., checking Lemma 1). This can be done, for example, by a run of the Bellman-Ford algorithm. Reweighting GR to obtain G R costs O(m) and the computation of D0 is O(n + m). Finding the SCCs of D0, along with computing a correspondence allowing each node to retrieve its SCC, takes O(n + m) (Gabow 2000). Checking Lemma 2 corresponds to verify whether there exists any red arc in some SCC. That is, for each y x < k we just need to check if the SCCs of y and x are the same (because any cycle in that SCC including that arc has weight zero). Thus, this step takes O(m). Likewise, checking Lemma 3 takes O(h) because we need to evaluate each F C = under the interpretation that sets to false all y x = k AF if and only if y and x are in the same SCC and π(y) π(x) = k. Computing DP takes O(n + m). To compute ε, scanning all atoms of S takes O(m + h). Finding a topological sort takes O(n + m) and finally computing a solution δ from the potential π takes O(n) (also when we make δ non-negative by rigid shifting). Overall, the complexity is O(nm + h). When dealing with strict inequalities only, then h = 0 and the bound boils down to O(nm). Notice that this is the time that Bellman-Ford needs to solve even a simple instance of STP. This is faster than (Gerevini and Cristani 1997) as their algorithm is based on Floyd-Warshall, whose complexity is O(n3) O(nm) regardless of the density of the graph. Experimental Evaluation In this section we provide a proof-of-concept implementation of our approach, comparing several variants of shortest paths algorithms. Then, we encode our model as a QF RDL formula since it is well-known that satisfiability of conjunctions of atoms y x k for { , <} is tractable. Therefore, this experimental evaluation offers a fair comparison2. As seen in Theorem 3, computing a feasible potential function π (or proving that none exists checking Lemma 1) is the most expensive step and costs O(mn). This is a strongly-polynomial bound, that does not depend in any way on the magnitude of the numbers in the input. Actually, these could be rather clumsy objects that we could prefer to let an oracle to manage. Still, the problem would be solved in at most O(mn) calls to the oracle. Although asymptotically optimal, Bellman-Ford with negative-cycle detection (from now on, BFTO) can be outperformed by other algorithms with the same time complexity but still better in practice: (Goldberg and Radzik 1993) combined with (Goldberg 1995) admissible-graph search negative-cycle detection algorithm (from now on, GORC); Bellman-Ford-Moore with (Tarjan 1981) subtree disassembly negative-cycle detection algorithm (from now on, BFCT). The interested reader is referred to (Bellman 1958; Ford Jr 1956; Moore 1959; Cormen et al. 2009) and to (Cherkassky and Goldberg 1999) for more details about the Bellman-Ford algorithm and for a survey about negativecycle detection algorithms, respectively. Another nontrivial step of our approach is the computation of SCCs; for that, we rely on (Gabow 2000), the fastest SCC algorithm according to (Alshomrani and Iqbal 2012). As a result, we have implemented three different versions of our approach using BFTO, GORC and BFCT, respectively. To get an idea about their performance, we have also implemented (Dutertre and de Moura 2006) s approach to handle strict inequalities through the symbolic computation of ε values. Again, we consider the three variants offered by BFTO, GORC and BFCT, since also (Dutertre and de Moura 2006) executes a non-modified SSSP algorithm combined with a negative-cycle detection procedure. Moreover, we included all SMT solvers that competed in the 15th International Satisfiability Modulo Theories Competition SMTCOMP 2020 for QF RDL (Model Validation Track and Single Query Track). These were: Yices2 v2.6.2 (Dutertre 2014), CVC4 v1.8 (Barrett et al. 2011), Math SAT5 v5.6.3 (Cimatti et al. 2013), z3 v4.8.8 (De Moura and Bjørner 2008), veri T v2016 (Bouton et al. 2009) and SMTInterpol v2.5 (Christ, Hoenicke, and Nutz 2012). To encode an instance S = (X, C , C<, C =) of ESTP, 2https://github.com/CALIPSO-Uni VR/estp-aaai2021 CPU Intel Core i7-6700K @ 4.00GHz RAM 64 GB DDR4 @ 2133MHz SSD Samsung SSD 850 EVO 1TB OS Arch Linux kernel 5.8.5-zen CXXFLAGS -O3 -march=native -std=c++17 Table 1: Benchmark environment. we simply convert it into the QF RDL formula: y x k C y x k y x