{'fraction_non_alphanumeric': 0.047092547092547093, 'fraction_numerical': 0.00731981981981982, 'mean_word_length': 4.095722483046426, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Incremental Satisfiability and Implication for UTVPI Constraints

Unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints which are polynomial time solvable (unless P=NP). There is considerable interest in their use for constraint solving, abstract interpretation, spatial databases, and theorem proving. In this paper we develop a new incremental algorithm for UTVPI constraint satisfaction and implication checking that requires O(m + n log n + p) time and O(n+m+p) space to incrementally check satisfiability of m UTVPI constraints on n variables and check implication of p UTVPI constraints.


Introduction
The unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints which are polynomial time solvable (unless P=NP). There is considerable interest in their use for constraint solving [7,6], abstract interpretation [9], spatial databases [11] and theorem proving [8]. In this paper we develop new incremental algorithms for UTVPI constraint satisfaction and implication.
A UTVPI constraint has the form ax+by ≤ d where x, y are integer variables, d ∈ Z and a, b ∈ {−1, 0, 1}. For example x+y ≤ 2, x−y ≤ −1, 0 ≤ −1 and x ≤ 2 are UTVPI constraints. UTVPI constraint solving is based on transitive closure: A constraint ax−y ≤ d 1 and y +bz ≤ d 2 implies the constraint ax+bz ≤ d 1 +d 2 . We can determine all the UTVPI consequences of a set of UTVPI constraints by transitive closure, but we need to tighten some constraints. The transitive closure procedure can generate constraints of the form x + x ≤ d and −x − x ≤ d, which need to be tightened to x ≤ d 2 and −x ≤ d 2 respectively. Jaffar et al. [7] and Harvey et al. [6] present incremental consistency checking algorithms for adding a UTVPI constraint c to a set φ of UTVPI constraints. They are based on maintaining the transitive and tight closure of the set of UTVPI constraints φ involving n variables. Both algorithms require O(n 2 ) time and O(n 2 ) space for an incremental satisfaction check. Both algorithms can also be used to incrementally check implication of UTVPI constraints by φ ∪ {c}. These algorithms require O(n 2 + p) time and O(n 2 + p) space for an incremental implication checking, where p is the number of constraints we need to check for implication. In order to (non-incrementally) check satisfiability of m UTVPI constraints on n variables these approaches require O(n 2 m) time, and to check implication they require O(n 2 m + p) time.
An improvement on the complexity of (non-incremental) satisfiability for UTVPI constraints was devised by Lahiri and Musuvathi [8]. They define a non-incremental satisfiability algorithm requiring O(nm) time and O(n + m) space. The key behind their approach is to map UTVPI constraints to difference constraints (also called separation theory constraints) of the form x − y ≤ d, where x and y are integer variables and d ∈ Z.
The difference constraints are a well studied class of constraints because of their connection to shortest path problems. We can consider the constraint x − y ≤ d as a directed edge x → y with weight d. Satisfiability of difference constraints corresponds to the problem of negative weight cycle detection, and implication of difference constraints corresponds to finding shortest paths (see e.g. [3] for details).
The mapping of UTVPI to difference constraints by Lahiri and Musuvathi [8] is a relaxation of the problem. The relaxed problem is solved by a negative (weight) cycle detection algorithm but it guarantees only the satisfiability in Q for the UTVPI problem. In order to check satisfiability in Z they need to construct an auxiliary graph and check for certain paths in this graph.
In this paper we first extend Lahiri and Musuvathi's algorithm [8] to check satisfaction incrementally in O(n log n + m) and O(n + m) space. Then we show how to build an incremental satisfiability and implication algorithm using the relaxation of Lahiri and Musuvathi and incremental approaches to implication for difference constraints of Cotton and Maler [3], which can incrementally check implication in O(n log n + m + p) time and O(n + m + p) space.

Preliminaries
In this section we given notation and preliminary concepts.
A weighted directed graph G = (V, E) is made up vertices V and a set E of weighted directed edges (u, v, d) from vertex u ∈ V to vertex v ∈ V with weight d. We also use the notation u d → v to denote the edge (u, v, d).
The path weight of a path P , denoted w(p) is Σ k i=1 d i . Let G be a graph without negative weight cycles, that is without a cycle P where w(P ) < 0. Then we can define the shortest path from v 0 to v k , which we denote by SP (v 0 , v k ), as the (simple) path P from v 0 to v k such that w(P ) is minimized.
Let wSP (x, y) = w(SP (x, y)) or +∞ if no path exists from x to y.
Given a graph G and vertex x define the functions δ ← and δ → x (y) = wSP (x, y) . Let G be a graph without negative weight cycles. Then π is a valid potential There are many algorithms (see e.g. [2]) for detecting negative weight cycles in a weighted directed graph, which either detect a cycle or determine a valid potential function for the graph.
Given a valid potential function π for graph G = (V, E) we can define the reduced cost graph rc(G) as (V, {(x, y, π(x)+d−π(y) | (x, y, d) ∈ E}). All weights in the reduced cost graph are non-negative and we can recover the original path length w(P ) for path P from x to y from paths in the reduced cost graph since w(P ) = w + π(y) − π(x) where w is the weight of the corresponding path in the reduced cost graph.
Since edges in the reduced cost graph are non-negative we can use Dijkstra's algorithm to calculate the shortest paths in the reduced cost graph in time O(n log n + m) instead of O(nm).

Difference constraints
Difference constraints have the form x−y ≤ d where x and y are integer variables and d ∈ Z. We can map difference constraints to a weighted directed graph. Definition 1. Let C be a set of difference constraints and let G = (V, E) be the graph comprised of one weighted edge x d → y for every constraint x − y ≤ d in C. We call G the constraint graph of C.
The following well-known result characterizes how the constraint graph can be used for satisfiability and implication checking of difference constraints.

Theorem 1 ([3]
). Let C be a set of difference constraints and G its corresponding graph. C is satisfiable iff G has no negative weight cycles, and if C is satisfiable then C |= x − y ≤ d iff wSP (x, y) ≤ d.
Definition 2. The transitive closure T C(φ) of a set of UTVPI constraints φ is defined as the smallest set S containing φ such that The tightened closure T I(φ) of a set of UTVPI constraints φ is defined as the smallest set S containing φ such that Table 1. Transformation from UTVPI constraint c to associated difference constraints D(c) to edges in the constraint graph E(c).
The tightened transitive closure T T C(φ) of φ is the smallest set containing φ that satisfies both conditions.
The fundamental result for UTVPI constraints solving is: We can extend this for implication checking straightforwardly:

Lahiri and Musuvathi's approach
Lahiri and Musuvathi map UTVPI constraints φ to difference constraints or equivalently a weighted directed graph G φ , and they use graph algorithms to detect satisfiability. We denote the constraint graph arising from φ as G φ = (V, E). The graph G contains two vertices x + and x − for every variable x. These variables are used to convert UTVPI constraints into difference constraints. The vertex x + represents +x and x − represents −x.
Let φ be a set of UTVPI constraints. Each UTVPI constraint c ∈ φ is mapped to a set of difference constraints D(c), or equivalently a set of weighted edges E(c). The mapping is shown in the Table 1. Each UTVPI constraint on two variables generates two difference constraints and accordingly two edges in the constraint graph. Each UTVPI constraint on a single variable generates a single constraint, and hence a single edge. Let −v denote the counterpart of a vertex v ∈ V , i.e. −x + := x − and −x − := x + . Clearly, for each edge (x, y, d) ∈ E the graph G φ also includes the edge (−y, −x, d) with equal weight. This correspondence extends to paths.
If we relax the restriction on variables to take values in Z and allow them to take values in Q we can check satisfiability in Q using G φ .
The reason why the feasibility in Z cannot be tested with G φ arises from the possible implication of constraints of the form The graph G φ ′ is shown in Figure 1(a). A zero length cycle is extracted in Figure 1(b). This cycle has solutions in Q but not in Z. 2 The satisfiability algorithm of Lahiri and Musuvathi [8] is based on Lemma 2 and the following result.

Lemma 3 ([8]).
Suppose G φ has no negative cycles and φ is unsatisfiable in Z. Then G φ contains a zero weight cycle containing vertices u and −u such that wSP (u, −u) is odd.
The algorithm first checks Q feasibility using a negative cycle detection algorithm, and then checks that no such zero weight cycles exists in G φ .
The complexity is O(nm) time and O(n + m) space assuming we use a Bellman-Ford single source shortest path algorithm [1,4] for negative cycle detection.

Incremental UTVPI Satisfaction
The incremental satisfiability problem is: Given a satisfiable set of UTVPI φ (with n variables and m constraints) and UTVPI constraint c, determine if φ∪{c} is satisfiable. In this section we define an incremental satisfiability checker for UTVPI constraints that requires O(n log n+m) time and O(n+m) space. It relies on simply making incremental the algorithm LaMu of Lahiri and Musuvathi.
The key is to incrementalize the negative cycle detection. We use an algorithm due to Frigioni et al. [5], using the simplified form (Algorithm 2: IncConDiff) of Cotton and Maler [3] (since we are not interested in edge deletion). Given a graph G = (V, E) and valid potential function π for G and edge e = u d → v, this algorithm returns G ′ = (V, E ∪ {e}) and a valid potential function π ′ for G ′ or determines a negative cycle and returns UNSAT. The complexity is O(n log n + m) time and O(n + m) space using Fibonacci heaps to implement argmin.

Algorithm 2: IncConDiff
Input: G φ = (V, E) a graph, π a valid potential function for G φ , edge (u, v, d) a new constraint to add to G φ . Output: UNSAT if φ ∪ {u − v ≤ d} is unsatisfiable, or G φ∪{u−v≤d} and a valid potential function π ′ for G φ∪{u−v≤d} . γ(v) := π(u) + d = π(v); The incremental UTVPI satisfiability algorithm simply runs IncConDiff at step 2 of LaMu, the remainder of the algorithm is unchanged. Since the remainder of the the LaMu algorithm requires O(n + m) time and space, the complexity bounds are the same as for the incremental negative cycle detection algorithm.

Incremental UTVPI Implication
The incremental implication problem is given a set P of p UTVPI constraints and a satisfiable set φ of m UTVPI constraints on n variables, where φ |= c ′ , ∀c ′ ∈ P , as well as a single new UTVPI constraint c, check for each c ′ ∈ P if φ ∧ c |= c ′ .
Incremental implication is important if we wish to use UTPVI constraints in a Satisfiability Modulo Theories (SMT) solver [10], as well as for uses in abstract interpretation and spatial databases. Our approach to incremental implication is similar to the approach of Cotton and Maler [3] for incremental implication for difference constraints.
The key to the algorithm are the following three results.
The result holds since tightening introduces constraints involving a single variable and any further transitive closure involving them can only create new constraints involving a single variable.
The result holds since any result of transitive closure on a new UTVPI constraint by ≤ d ′ introduced by tightening, can be mimicked using the constraint by + by ≤ {2d ′ , 2d ′ + 1} that introduced it, and tightening the end result.
The above two results show that T C(φ) is the crucial set of interest for UTVPI implication checking. The following result shows how we can use the constraint graph to reason about T C(φ).
Proof. This lemma follows straightforward of the definition of T C(φ) and the transformation of the set of UTVPI constraints to its constraint graph. It can be prove easily by induction over the number of transitive closure steps in T C(φ) resp. the length of cycle or path in G φ . 2 Example 4. Consider φ of Example 1. Then for example x + x ≤ 1 ∈ T C(φ) and there is a path x − x + of length 1 in G φ shown in Figure 1(c). Similarly y − z ≤ −5 ∈ T C(φ) and there are paths y − z − and z + y + of length −5 in G φ .
We can use paths (in particular shortest paths) in G φ to reason about most constraints in T T C(φ). In order to handle tightening we introduce a bounds function ρ which records the upper and lower bounds for each variable x, on the vertices x + and x − . It is defined as: We can show that ρ(x − ) computes the the upper bound of x and −ρ(x + ) is the lower bound of x. Using Lemmas 5 and 6 we have.
where we assume min ∅ = +∞. The key to incremental satisfaction is the following result.
Proof. Let φ be a satisfiable set of UTVPI constraints in Q. Because of the Lemma 6 it applies the non-existence of a constraint 0 < d ∈ T C(φ) where d < 0. Therefore φ is unsatisfiable in Z iff such a constraint belongs to T T C(φ) \ T C(φ) (Theorem 2), i.e. a possible unsatisfiability is caused by tightening.
The Lemma 4 implies the equivalence for each constraint Effectively failure can only be caused by tightening if the bounds of a single variable contradict.
Example 6. Consider the graph in Figure 1(a) for constraints φ ′ of Example 2. There is no negative weight cycle in G φ ′ but ρ(x − ) = 0 and ρ(x + ) = −1 because Similarly the key to incremental implication is the following rephrasing of Corollary 1.

Theorem 4. If φ is a satisfiable set of UTVPI constraints then
Proof. Let φ be a satisfiable set of UTVPI constraints. Because of Corollary 1 it holds φ |= c and c ≡ ax Now, the theorem holds straightforward due to Lemma 7 for the constraints with one variable, and Lemma 4 and 6 for the other constraints. Algorithm 3 shows the new algorithm. As input it takes the constraint graph G φ , a valid potential function π, the bounds function ρ, a set P of UTVPI constraints to check for implication, as well as the UTVPI constraint c which should be added to φ.
In the first step (line 1) the constraint c is transformed to its corresponding edges E(c) in a constraint graph. Then each edge in E(c) is added consecutively to the constraint graph G φ by using the IncConDiff algorithm of Cotton and Maler [3]. After inserting all edges in G ′ , the constraint graph equals to G φ∪{c} and π ′ is its valid potential function for G ′ . Hence φ ∪ {c} is satisfiable in Q. The remainder of the algorithm maintains the bounds function ρ ′ (lines from 8 to 12) and it is used to test the feasibility in Z (lines 13 and 14), and the implication of constraints in P (lines 15 to 18).
By Lemma 6 to maintain ρ we need to see if the shortest path from x to −x has changed. We only need to scan for new shortest paths using the newly added edges. We can restrict attention to a single added edge (u, v, d) since if there is a path from x over the edge (u, v, d) to Proof. The algorithm is correct if it returns UNSAT in the case of unsatisfiability of φ ∪ {c} or the constraint graph G φ∪{c} , its valid potential function π ′ , its bounds function ρ ′ and the set of constraints P ′ ⊆ P not implied by φ ∪ {c}. The Lemma 2 and the Algorithm IncConDiff (see Cotton and Maler [3]) guarantee that after termination of IncConDiff G ′ = G φ∪{c} and π ′ is its valid potential function if φ ∪ {c} is satisfiable in Q; otherwise φ ∪ {c} is unsatisfiable and the algorithm returns UNSAT.
After application of IncConDiff the algorithm maintains the bounds function (lines 8 to 12) by calculation of the shortest path x u → v −x via one added edge (u, v, d) ∈ E(c) for each node x in G φ∪{c} . Remark: we only have to considered the shortest paths via the added edges ρ give us the length of a shortest path without those added edges. Due to Theorem 3 the algorithm checks φ ∪ {c} for unsatisfiability in Z in the next two lines. If it is unsatisfiable ScSt terminates and returns UNSAT.
The remainder of the algorithm computes the set of non-implied constraints P ′ ⊆ P by testing for all constraints c ′ ∈ P if the length of both paths x u → v y, −y u → v −x are longer than d ′ and the sum of the upper bounds ρ ′ (x) + ρ ′ (−y) is greater than d ′ where (x, y, d ′ ) ∈ E(c ′ ). If all three cases hold then c ′ is not implied by φ ∪ {c} thanks to Theorem 4.
The run-time is determine by the run-time of IncConDiff, the calculation of δ ← u , δ → v which are O(n log n + m), and the implication check O(p). All the other computations can be done in constant or linear time with respect to n and m. So the overall run-time is O(n log n + m + p). 2 The cost of IncConDiff and the shortest path computations are each O(n log n+m), while the implication checking is O(p). The space required simply stores the graph and implication constraints.

Experimental Results
We present empirical comparisons of the algorithms discussed herein, first on satisfaction and then on implication questions.
For both experiments we generate 60 UTVPI instances φ in each problem class with the following specifications: the values d range uniformly in from −15 to 100. approximately 10% are negative, each variable appears in at least one UTVPI constraint, each constraint involves exactly two variables, and there is at most one constraint between any two variables two variables are allowed.
In addition, for the implication benchmarks 10 implication sets P of size p were created for each n using the same restrictions as defined above. On average over all benchmarks, 65% of the constraint P were implied by the corresponding φ.
The experiments were run on a Sun Fire T2000 running SunOS 5.10 and a 1 GHz processor. The code was written in C and compiled with gcc 3.2.
We run incremental satisfiability on a system of m constraints in n variables, adding the constraints one at a time. We compare: IncLaMu the incrementalization of LaMu presented in Section 4, ScSt the incremental implication checking algorithm of Section 5 where p = 0, mLaMu running LaMu m times for m satisfaction checks, and HaSt the algorithm of [6]. The results are shown in Table 2, where d represent the density of a UTVPI instance. We split the examples into cases that are feasible, Z infeasible, and Q infeasible. Moreover, the table entry "all" shows the overall average run-time and the number of examples for each case in the same ordering as above written. Interestingly for dense satisfiable systems HaSt is best, but overall IncLaMu is the clear winner.
The incremental implication checked satisfiability and the implications of constraints P incrementally as each of the m constraints were added one at a time. A run was terminated if there were no more constraints to add, all constraints in P were implied, or unsatisfiability was detected. We compare the two algorithms that can check implication: ScSt versus HaSt. Table 3 shows the results. Overall the checks for implication are cheap compared to the satisfiability check for each algorithm. Hence the results are similar to the satisfiability case. Again HaSt is superior for dense systems, while ScSt is the clear winner on sparse systems.