A Divide-and-Conquer Approach for Solving Interval Algebra Networks

1 Introduction

Temporal information such as "the financial crisis begun during the 2008 presidential campaign" does not specify exact dates or durations; only qualitative information about the relationships between different periods of time is given. Allen [1983] introduced the Interval Algebra (IA), a qualitative calculus to represent and reason about such relationships between temporal intervals. It distinguishes 13 atomic relations, i.e., between any two temporal intervals exactly one of these relations holds. Allen's approach was very successful and marked the start of a new research area, now called qualitative spatio-temporal reasoning (QSTR).

QSTR uses constraint calculi to reason about spatial and temporal information. The fundamental reasoning task in QSTR is to decide whether a given collection of information is consistent. This can be formulated as a constraint satisfaction problem. Fig. 1a depicts a simple example that is represented as a constraint network over IA: "Peter reads the newspaper during breakfast, and goes to work after breakfast." This information is clearly consistent; Fig. 1b depicts a solution where each variable has been instantiated to a concrete time interval. However, for large and complex networks, which may contain disjunctions of atomic relations such as

"Peter reads his private email either before or after work," we will need temporal reasoning algorithms to decide consistency.

Deciding consistency in QSTR is NP-hard for many calculi including IA. If only atomic IA relations are permitted, however, the consistency problem becomes tractable. Specifically, it has been shown that the path consistency algorithm, which removes impossible relations from all triples of nodes in a constraint network, is sufficient for deciding consistency for atomic IA networks, i.e., networks where each edge is an atomic relation.

In the past twenty years there have been many attempts to make reasoning in IA and other spatial or temporal calculi more efficient. Most of these approaches use constraint satisfaction techniques where an instance is solved by backtracking over tractable sub-instances. More efficient solutions were obtained by studying different backtracking heuristics and most notably also by enlarging known tractable subsets-sets of relations for which the consistency problem is tractable [Nebel and B¨urckert, 1995]. By combining different backtracking heuristics and the maximal tractable subset of IA, many instances, even hard ones in the phase-transition region, were solved reasonably fast [Nebel, 1997]. However, particularly large instances remain difficult to solve.

Pham et al. [2008] recently proposed an encoding of IA networks into Boolean formulas such that the formula is satisfiable if and only if a path-consistent atomic refinement of the network exists. The encoding enforces path consistency using a set of clauses for every triple of nodes in the network, and solution finding is delegated to an off-the-shelf SAT solver. This results in increased efficiency for some hard problem instances, but its memory requirements can be quite demanding as the encoding grows cubically with network size. Our experiments showed that for large instances the SAT formulas can easily become too large even for modern SAT solvers.

In this paper we present a theoretical analysis that results in a divide-and-conquer approach to solving IA networks. The basic idea is that under certain conditions, which IA satisfies, one can decompose a network into two overlapping subnetworks, and solve the two sub-networks separately. This eliminates the need for examining triangles across the two sub-networks when enforcing path consistency. The same idea applies recursively to each of the sub-networks, leading to further savings. Combining this result with the approach of [Pham et al., 2008] we are then able to produce significantly more compact SAT encodings and more efficient solutions.

In the following section we review the basic notions of qualitative spatial and temporal calculi and summarize existing constraint-based and SAT-basedmethods. In Section 3we present a theoretical analysis of IA that leads to a divide-andconquer SAT encoding scheme for IA networks. In Section 4 we empirically evaluate the resulting SAT encoding and show that it is superior to existing solvers on hard instances. Section 5 concludes the paper.

2 Preliminaries

An IA network describes possible scenarios of intervals along a directed line. The network is a complete graph with vertices representing the intervals, and directed edges representing the possible relationship between them. As in our earlier example of Fig. 1a, we often omit edges where the relationship between the two intervals is the universal relation (i.e., no constraint is specified). Also note that we only need to give one directed edge between a pair of vertices as the other one is implied.

More formally, a qualitative temporal (or spatial) calculus A represents relationships between temporal (or spatial) entities from a given domain D, such as intervals, points, or extended regions. A calculus partitions D×D into a finite set of pairwise disjoint and jointly exhaustive atomic relations B, i.e., between any two elements of D exactly one atomic relation holds. Temporal or spatial information can then be represented in the form of constraints xRy, where x and y are variables over D and R ∈ 2B is a disjunction of atomic relations. Disjunctions are used to represent indefinite information. If the exact relationship between x and y is known, then R is an atomic relation.

IA [Allen, 1983] is the best known example of a qualitative calculus. Its domain is the set of intervals on a directed time line, the 13 atomic relations are {before, after, meets, metby, overlaps, overlapped-by, equals, during, includes, starts, started-by, finishes, and finished-by}, leading to 213 = 8192 possible IA relations.

A set of binary constraints Θ of a qualitative calculus A can be represented as a binary constraint network N = (VN, ℓN) over A, where the variables of Θ become the vertices VN of N and ℓN(i, j) = Rij labels the edge between nodes i and j, where Rij denotes the constraint between variables i and j. Note that Rij is the universal relation in case no constraint is imposed between variables i and j.

A network N is a sub-network of another network M if VN ⊆ VM and the labeling ℓN of the edges of N is exactly the same as the labeling ℓM of the same edges in M, i.e., ℓN(i, j) = ℓM(i, j)∀i, j ∈ VN. We write N ⊆ M in such cases. N is a refinement of M if VN = VM and ℓN(i, j) ⊆ ℓM(i, j)∀i, j ∈ VN. The intersection (∩) of two networks N1,N2 is the maximal network that is a subnetwork of both N1 and N2. When the two networks satisfy VN1 ∩ VN2 = VN1∩N2 , we also define their union (∪) to be the minimal 1 network of which both N1 and N2 are sub-networks. A network N is atomic if all the labels of N are atomic relations of A, and is path consistent if Rij ⊆ Rik ◦ Rkj∀i, j, k ∈ VN , where ◦ is the composition operator of A (the composition R◦S of two relations is defined as the relation {(a, c)|∃b : (a, b) ∈ R, (b, c) ∈ S}).

2.1 Deciding consistency

The fundamental reasoning problem for a qualitative calculus is that of deciding consistency for a set of constraints Θ, i.e., deciding whether there is an instantiation of all variables in Θ with values from the domain D such that all constraints in Θ are satisfied. As domains of a qualitative calculus such as IA are usually infinite, standard constraint propagation methods do not directly apply. Instead, we can use operators on the relations in order to derive new information from the given constraints.

An example of such a technique is the well-known path consistency algorithm, which iteratively checks all triangles in the network to rule out impossible relations until a fixed point is reached. Continuing with our example, given that "reading" occurs during "breakfast" and "work" occurs after "breakfast," path consistency will detect that it must be the case that "reading" occurs before "work," after eliminating the other 12 atomic relations that are initially in the label. As no other relations on any of the edges can be eliminated, the network is now path consistent.

IA has the property that for any atomic network of size n, path consistency implies strong n-consistency [van Beek and Cohen, 1990]. This means that given a path-consistent atomic network and any subset of its variables (nodes) of size k, any consistent instantiation of k - 1 variables in the set can be extended to a consistent instantiation of all k variables. This reduces consistency checking to a search for a path-consistent atomic network that is a refinement of the original network.

2.2 Constraint-based approach

The basic constraint-based approach for IA networks is hence a backtracking search where branching is performed on the atomic relations in the label of each edge. Path consistency is enforced immediately after each branch is created, and any inconsistency thus detected results in backtracking. The network is consistent if and only if a leaf of the search tree can be successfully reached where every edge has been assigned an atomic relation. Variable and value ordering heuristics for these algorithms have been studied to improve their efficiency [Ladkin and Reinefeld, 1992].

1 Minimality here means that the network has the fewest vertices and the fewest edges possible, where we regard edges labeled with universal relations as invisible.

The major improvement in the efficiency of constraintbased solvers has been the use of large and preferably maximal tractable subsets of the full set of relations. Consistency for networks that contain only relations from such sets can be decided in polynomial time, often with the path consistency algorithm. The only maximal tractable subset (ORD-Horn) of IA that contains all atomic relations has been identified by Nebel and B¨urckert [1995]. Nebel [1997] showed that the right combination of tractable subset and heuristics can lead to very fast solutions. This result led to an increased interest in identifying tractable subsets for other qualitative calculi [Renz and Li, 2008].

While Nebel's solver has been the standard IA solver for the past ten years, recent improvements have been proposed [Condotta et al., 2007] and implemented in the latest version of the GQR solver [Gantner et al., 2008], which is currently the fastest constraint-based IA solver.

2.3 SAT-based approach

Recently, Pham et al. [2008] proposed an encoding of IA networks into Boolean formulas. The encoding can be based on either the constraints between the intervals as given in the network (event-based), or the constraints between the end-points of those intervals (point-based). In either case, the Boolean formulas are constructed in such a way that each solution of the formula corresponds to a path-consistent atomic refinement of the network, and vice versa. Hence the formula is satisfiable if and only if the network is consistent.

They studied several alternative encoding methods and found that empirically the "point-based 1D support" encoding performs best. The "1-D support" encoding works by allocating a Boolean variable xvij for every atomic relation v on the edge between two intervals (i, j). The variable is true if and only if the corresponding atomic relations holds between i and j in the final solution of a path-consistent atomic network. Two sets of at-least-one (ALO) and at-most-one (AMO) clauses are introduced to ensure that exactly one of these atomic relations holds in the final solution:

To ensure the final network is path consistent, a set of support (SUP) clauses is introduced to encode that every triangle (i, j, k) of the network (regarded as a complete graph) be closed under composition and intersection:

In the point-based encoding, one includes the same set of clauses as above, but for the point algebra (PA) instead of IA, prescribing the relations between the endpoints of the intervals. The variable xui-j-, for example, denotes the atomic relation u between the starting points of intervals i and j (substitute + for - for the ending points). To ensure soundness, this encoding requires an additional set of clauses to forbid spurious IA relations introduced by the intervals-to-points translation:

In their empirical study of IA networks of up to 100 nodes, Pham et al. [2008] have shown that the "point-based 1-D support" encoding used in conjunction with the MiniSat SAT solver outperforms Nebel's solver with its default settings on many hard instances.

3 A new divide-and-conquer approach

As mentioned earlier, a weakness of the SAT-based approach is the size of the encoding, which for large networks can outgrow available memory or can make SAT solving otherwise inefficient. In particular, many networks are not densely connected (the missing edges implicitly represent universal relations) and the encoding must nevertheless treat the network as a complete graph and generally include clauses for all its triangles, leading to a cubic complexity in all cases.

Our solution to this issue starts with a new theoretical result about how two consistent networks sharing a common sub-network can be amalgamated into a larger consistent network, provided a particular property holds. We then present a method that uses this result and recursively partitions a network into small sub-networks before they are individually encoded into Boolean formulas, thus avoiding the need to include many triangles across the sub-networks that have edges labeled by universal relations.

3.1 Amalgamation of networks

Previously, Li et al. [2008] analysed the problem of combining networks in QSTR without introducing inconsistencies. They introduced the Network Amalgamation Property (NAP), which guarantees that two networks over a calculus can be amalgamated into a larger network such that applying path consistency to the resulting network does not change any existing constraints. Here we consider a form of NAP where we restrict the two networks and their amalgams to be atomic networks. We call this the Atomic Network Amalgamation Property (aNAP).

Definition 1 (Atomic Network Amalgamation Property)

A qualitative calculus A has aNAP if for any pathconsistent atomic networks N1 and N2 over A such that VN1 ∩ VN2 = VN1∩N2 , N1 ∪ N2 has a path-consistent atomic refinement.

Fig. 2 illustrates this property. Consider the networks N1 and N2 over a calculus A having aNAP shown in Fig. 2a, with their intersection shown on the far left. Their union N1∪ N2 is shown in Fig. 2b, where the dotted edge represents the universal relation and all other edges are those from N1 and N2. The dotted edge is the only edge with a non-atomic label and aNAP guarantees the existence of an atomic refinement of the edge that results in a path-consistent atomic network.

Next we establish the following sufficient condition for aNAP, and show that it is satisfied by both IA and PA.

Theorem 1 A qualitative calculus has aNAP if path consistency implies strong n-consistency for all atomic networks of size n over the calculus.

Proof. Given a qualitative calculus A satisfying the above condition and two path-consistent atomic networks N1 and N2 over A such that VN1 ∩VN2 = VN1∩N2 , let N0 = N1∩N2

and M = N1 ∪ N2. We wish to show that M is consistent, which will establish aNAP. Take any consistent instantiation α1 of N1, and consider its projection α0 on VN0 . Since N2 is strongly |VN2 |-consistent, α0 can be extended to a complete consistent instantiation α2 of N2. The extension will not conflict with α1 because none of the additional variables are in VN1 (since VN1 ∩VN2 = VN0 ). Hence the combination of α1 and α2 is a consistent instantiation of M.

Corollary 1 IA and PA have the aNAP property.

Proof. Path consistent atomic networks of size n in IA and PA are guaranteed to be strongly n-consistent [van Beek and Cohen, 1990]. Hence both have the aNAP property.

3.2 Partitioning networks: reverse amalgamation

The above results allow us to amalgamate two networks into a larger network while preserving consistency. In this work we are interested in a divide-and-conquer method for networks, i.e., exactly the opposite of amalgamation: we want to take a large network and partition it into smaller networks such that their consistency can be used to decide the consistency of the larger network. The following theorem, directly derivable from the definition of aNAP, formalizes this idea.

Theorem 2 Given a qualitative calculus A for which aNAP holds and for which path consistency implies consistency of atomic networks, a network M over A is consistent if there exist networks M1,M2 such that M1 ∪M2 = M, M1 has a path-consistent atomic refinement N1, M2 has a pathconsistent atomic refinement N2, and N1 ∩N2 is a refinement of M1 ∩ M2.

Given that aNAP holds for a qualitative calculus, this theorem allows us to partition a network M into two overlapping sub-networks N1 and N2 that satisfy VN1 ∩ VN2 = VN1∩N2 and N1 ∪ N2 = M. When deciding path consistency, we can then disregard all triangles with at least one edge (labeled with the universal relation) between VN1 \ VN1∩N2 and VN2 \ VN1∩N2 . This applies recursively to each sub-network while we ensure that the intersection of the two sub-networks from any previous level stays together (to retain soundness).

We can stop the partition at any stage (or continue until no networks can be partitioned anymore) and then encode the remaining triangles using the existing SAT encoding of [Pham et al., 2008]. Theorem 2 guarantees the soundness of the new encoding; completeness is also retained as the new encoding only disregards triangles in the network.

3.3 Partitioning networks: an example

In the following we give an example that demonstrates our partitioning method and how it leads to a smaller SAT encoding. Consider the network M of eight nodes {v1 . . . v8} over either IA or PA in Fig. 3a, where edges labeled with universal relations are omitted. Recall that the basic SAT encoding must view the network as a complete graph and hence consider triangles over all edges including the invisible ones. Our goal is to show how some of those triangles can be ignored.

Let us make a cut through M as shown by the dotted line, breaking the network into the sub-network N2 (Fig. 3c) on the right, and N1 (Fig. 3b) on the left. Note that we have added to N1 all the endpoints of the cut edges from the other side together with the incident edges; this is to ensure that N1 ∪ N2 = M.

Theorem 2 implies that we need only encode N1 and N2 separately as long as we ensure that their respective solutions agree over their intersection. This condition is automatically ensured in the SAT encoding as long as we encode the intersection of N1 and N2 only once (while encoding the remainders of N1 and N2 separately). This immediately allows us to ignore a total of 21 triangles, namely those that include at least one (invisible) edge from {v1, v2, v3} to {v7, v8}.

We can apply the same idea recursively to each of the subnetworks. Let us proceed with N1 for example. In recursion we need to take one additional measure, namely to ensure that the intersection of the two sub-networks previously created stays together. In this example, that is to say that we cannot split v4, v5, and v6 when partitioning N1. Fig. 4.b gives a feasible partitioning in this regard, allowing us to further ignore 3 triangles: (v1, v4, v5), (v1, v4, v6), and (v1, v5, v6).

In the end, we avoid encoding 24 out of the 56 triangles compared with the original approach of [Pham et al., 2008].

3.4 Partitioning heuristics

In general there are multiple ways to partition a given network. Our goal is to find "good" partitions, for example with a small overlap and a good balance between the two subnetworks, both of which tend to maximize the number of triangles that can be disregarded. Our implementation uses the software tool hMETIS [Karypis and Kumar, 1998]. hMETIS heuristically minimizes the number of edges being cut while producing a relatively balanced cut, which serves well to help achieve our goal. 2

4 Empirical evaluation

We benchmarked the performance of our partitioned SAT encoding with the original SAT encoding from [Pham et al., 2008], as well as two constraint-based solvers, the one from Nebel [1997] and the GQR-994 solver [Gantner et al., 2008], with their best-performing heuristics enabled. In particular, Nebel's solver was run with options {static, global, queue} enabled, which had been shown to vastly improve the performance over default settings of the program in [Nebel, 1997]. MiniSat v2.070721 [E´en and S¨orensson, 2003] was used to solve the CNF formulas generated by the SAT encodings. All our test instances were randomly generated networks around the phase-transition region with a given number of nodes and average degree, and an average label size of 6.5. Furthermore, we tested only networks that were not found inconsistent by path consistency. The tests were ran on 2.4 GHz processors with a 2 hour time limit and a memory limit of 2 GB.

4.1 Smaller networks

In the first part of the experiment we tested 27,000 IA networks with from 50-100 nodes and degrees from 8-12. We tested the event-based and point-based encodings of both the original and partition-based approaches. Out of all the tests only Nebel's solver failed on 9 instances; every other solver managed to solve all the instances.

The size of the Boolean formula generated in terms of number of clauses for each encoding is shown in Fig. 5. The data confirms that point-based encoding generates smaller CNF formulas than the event-based encoding for the same network. It also shows that the number of clauses generated from the our partitioned encoding is roughly half that from the encoding of [Pham et al., 2008], and our event-based partitioned encoding produces about as many clauses as their point-based encoding.

2 The parameters used in calling hMETIS are: options[] = {1, 10, 1, 1, 1, 0, 0, 1, 0}, and ubFactor = 35; in recursion we set options[6] = 1 and specify a set of nodes that needs to stay together.

Fig. 6 compares the performance of all solvers. It confirms that the constraint-based approaches of Nebel and GQR solve easy instances very efficiently, whereas our point-based partitioned encoding dominates all other approaches in average CPU time on the harder instances.

4.2 Larger networks

In the second part of the experiment we generated 100 networks of size 110 to 200 with an average label size 6.5 for each degree from 8 to 12. In particular, we focused on the phase-transition region which was identified to be between degrees 10 and 11.5. We recorded the number of instances solved by each solver within the time and memory limit, and the time taken to solve them.

Fig. 7 plots the number of instances solved against network degree, showing that the partitioned encoding dominates all other solvers for networks of any degree. The superior scalability of the partitioned encoding is further illustrated in Fig. 8, which focuses on the hard region and plots the number of instances solved against network size.

To further complete the picture, Fig. 9 shows the number of instances solved against CPU time. The constraintbased approaches of Nebel and GQR solved a large number of instances very quickly, but struggled to solve the harder instances even when more time was available. The point-based encoding of [Pham et al., 2008] performed better than Nebel's solver, but was inferior to GQR. Once again our point-based partitioned encoding solved more instances than all the other approaches, and solved most instances under 1 hour.

5 Conclusion and future work

Based on the idea of divide-and-conquer, we proposed a new method for encoding constraint networks over IA into SAT. The method relies on a special property of IA that allows two atomic networks over IA to be consistently amalgamated over a shared sub-network. We created a program that uses this property to partition networks over IA to produce compact SAT encodings. The empirical evaluation shows that our partitioned encoding dominates existing approaches in efficiency and scalability on difficult IA instances.

In general, reduced formula size does not necessarily lead to faster SAT solving. While our results indicate that detecting and removing redundant clauses via partitioning is indeed beneficial, a second interesting observation can be made regarding the correlation of encoding size and solution time: As Pham et al. [2008] have previously observed and we again confirmed, the point-based encoding in fact leads to both smaller formulas and faster solutions than the eventbased encoding whether or not partitioning is employed. This is apparently due to PA being a much smaller algebra-the smaller composition table leads to fewer clauses required per triangle for a given network. This indicates that SAT-based approaches may be made more efficient if a network can be translated into another one over a smaller calculus.

In this paper we demonstrated the usefulness of our method for solving IA networks. However, our method is applicable to any qualitative calculus for which path consistency implies consistency for atomic networks and for which aNAP holds. While the former property holds for many calculi, it is far less known where the latter holds. We presented a sufficient condition (Theorem 1) for aNAP, but it remains unclear whether it is also necessary. Another question is whether a purely syntactic and automated proof for aNAP exists, which would allow us to automatically identify calculi to which our partitioning method is applicable.

Acknowledgments

National ICT Australia is funded by the Australian Government's Backing Australia's Ability initiative, in part through the Australian Research Council.