StarVars - Effective Reasoning about Relative Directions

1 Introduction

Research in qualitative spatial reasoning (QSR) develops the theoretical foundations for abstract, symbolical representation and reasoning with spatial knowledge. Most spatial representations developed in QSR are so-called qualitative calculi [Ligozat and Renz, 2004b], which are spatial logics in the sense of [Aiello et al., 2007] with the syntax of a constraint language, i.e., qualitative representations are conjuncts of constraint relations. A fundamental reasoning task for such representations is that of deciding consistency, i.e., to compute a yes/no answer to the question whether a spatial model exists that satisfies all constraint relations.

From the perspective of applications in autonomous agents, representations that can handle directional knowledge are particularly important. Directional knowledge describes the po- Diedrich Wolter University of Bremen Germany dwolter@sfbtr8.uni-bremen.de sition of an object relative to the position and orientation of an observer, i.e., it uses an ego-centric frame of reference which allows observations of an agent to be described. This is essential for many navigation problems, including interpreting route directions and representation and reasoning with navigation rules. In the last 20 years, various approaches to representing directional knowledge have been proposed, starting with the works [Freksa, 1992; Ligozat, 1993] to, more recently, [Moratz, 2006; Mossakowski and Moratz, 2012]. It was however discovered that deciding consistency for these representations is NP-hard and it remains an open question whether an NP algorithm exists [Wolter and Lee, 2010]. Moreover, previous research has focused on deciding consistency of a qualitative representation, the question of how a spatial model can be computed remains largely unanswered.

∗Financial support by DFG (SFB/TR 8 Spatial Cognition, project R3-[Q-Shape]) is acknowledged.

This poses a severe limitation for human machine interaction, since it is not possible to visualize the represented spatial knowledge.

In this paper we develop the new constraint language StarVars, which allows us to represent relative direction knowledge of arbitrary granularity and accuracy.

We present an NP algorithm that computes a spatial model for a given StarVars constraint formula and fails if and only if the constraint formula is unsatisfiable. Doing so, we obtain an important answer to the two longstanding questions of how one can reason effectively with relative direction relations and how to present this knowledge visually.

2 Qualitative Spatial Reasoning

In QSR, constraint languages are used to represent spatial knowledge [Cohn and Renz, 2008]. Let a constraint language L defined as a finite collection R of binary relations on an infinite domain of spatial entities D. A central problem of QSR is solving the constraint satisfaction problem for L (CSP(L) for short), i.e., deciding the satisfiability of a formula

where v1, . . . , vn are variables defined on D, and each Rij is a finite union of members of R. 1 We call Rij a relation of L and formula (1) a CSP(L) instance. If Rij is the union of all members of R, we call it the universal relation of L. If Rij involves only one member of R, then Rij is said to be an atomic relation of L, and we call a CSP(L) instance atomic, if all of its relations Rij are atomic. Typically, in view of composition-based constraint propagation as reasoning method [Renz and Nebel, 2007], the members of R are supposed to be jointly exhaustive and pairwise disjoint (JEPD) 2 and form a partition scheme [Ligozat and Renz, 2004a]; a constraint language with this property is called a qualitative calculus.

1 CSP(L) for ternary or n-ary relations is defined analogously.

2.1 Cardinal Direction Relations

One example of a spatial constraint language is ST AR that represents qualitative directions between points in the plane [Renz and Mitra, 2004]. For each point p, ST AR defines a number of direction sectors and half-lines that determine the spatial relationship of other points q with respect to p (see Figure 1a). The qualitative direction constraint pRq is the sector (or the half-line) R in which q is located relative to p. ST ARm allows us to adjust the granularity by varying the number m of lines that determine the direction sectors. The angular range of the sectors may be chosen freely, but commonly all sectors are equally large.

Given a choice of sectors, all direction information between any two points is expressed with respect to these sectors and half-lines whose orientation is globally aligned. Therefore, ST AR relations are cardinal direction relations that do not depend on the orientation of the points.

2.2 Relative Direction Relations

Relative direction relations describe directions between two objects relative to a reference object. The most elementary system of directional relations is called FlipFlop or LR [Ligozat, 1993], see Figure 1b. The qualitative relations of LR are defined based on a reference system generated by a directed line connecting two points. The position of a third point is then categorized as to be either left or right of the line, or on 5 different segments of the reference line (two additional relations describe degenerate cases and are omitted here). Other point-based approaches like, for example, the direction relations "double cross" [Freksa, 1992] or TPCC [Moratz and Ragni, 2007] are refinements of LR relations.

Binary relations are sufficient to determine relative directions for objects comprising an intrinsic direction (e.g., the island is on the starboard side of a sailing ship). Domains considered in QSR are, for example, directed lines or oriented points, i.e., points that have been equipped with an orientation. One particularly interesting representative of this class is the set of OPRAm relations [Moratz, 2006], which is based on the domain R2 × [0, 2π) of oriented points. Half-lines and angular sectors are instantiated to describe the position of one oriented point as seen from another. The relations of OPRAm are defined with respect to a granularity parameter that determines how many sectors are used (OPRAm uses m lines to divide the full circle evenly, giving 2m angular sectors and 2m half-lines). Figure 1c presents an example of an OPRA2 relation ∠17 . In the example, B is located in sector 7 as seen fromA, which, in turn, is located in sector 1 as seen from B. OPRAm is very similar to ST AR, but the sectors in OPRAm depend on the relative orientation of the point, while for ST AR their direction is globally fixed.

2 A set of relations is JEPD, if for each pair of elements (x, y) ∈ D×D, there is one and only one relation of R that contains the pair.

While representing knowledge in an ego-centric frame of reference is well-suited for applications with navigating agents, reasoning with relative direcions is not tractable. Even for the most elementary set of LR's directional relations "left of" and "right of" the problem of deciding whether an atomic instance of CSP(LR) is consistent is NP-hard [Wolter and Lee, 2010], while NP-membership has not been shown so far. Since all known point-based relative direction calculi are more expressive than LR they are all NP-hard and their NP-membership remains unclear as well. From the perspective of a practitioner wanting to utilize relative directional knowledge it may be even more impeding that no effective decision procedure is known so far. In particular, the composition-based reasoning widely used in QSR is ineffective for deciding consistency of CSPs involving directional relations [L¨ucke et al., 2008].

3 The Spatial Constraint Language SVm

We will now define StarVarsm or SVm-a constraint language for relative direction relations that integrates the expressiveness of relative direction representation with the wellbehaved properties of cardinal directions. The relations of SVm are obtained by generalizing ST ARm relations to accommodate for relative direction information. Our idea is to retain the fixed arrangement of sectors given by ST ARm relations but to interpret directions with respect to an observer's orientation. An example of two SV8 objects are shown in Figure 2a.

In detail, the constraint language SVm is defined over the domain R2 × Θm, where m ∈ N,m ≥ 2 is the granularity parameter and Θm = {k· 360◦ m |k = 0, 1, . . . ,m-1} the orientation domain. Given an oriented point A = (xA, yA, θA) ∈ R2 ×Θm, the value of (xA, yA) ∈ R2 determines the position and the value of θA ∈ Θm the angle of the orientation of A. In Figure 2b an oriented point A in SV8 is illustrated with θA = 90◦ . By definition the higher the value m, the finer adjustable is the orientation of an SVm object.

We define relations in SVm as follows. Given a pair of oriented points, the position of the second point is described with respect to the first point which serves as reference. To this end, we partition the plane into m evenly sized angular sectors centered at the reference point-see Figure 2a for illustration. The sectors of the reference point are bounded by m-1 half-lines numbered 0, 1, . . . , m-1 counterclockwise with half-line 0 aligned with the orientation of the reference point. Sector s is bounded by half-lines s and s + 1 (mod m), where half-line s belongs to that sector and half-line s + 1 (mod m) does not. Oriented points A and B are said to be in relation [[s]] if B is positioned in sector s of A. Additionally, we establish a special relation S for the case of super-position, i.e. for two oriented points sharing the same position in R2 but not necessarily the same orientation. In summary, relations [[0]], [[1]], . . . , [[m- 1]], S constitute the JEPD set R of atomic relations in SVm.

We will use the notation [[c..d]] as an abbreviation of relation [[c]] ∪ [[c + 1]] ∪ · · · ∪ [[d - 1]] (i.e., the angular sector bounded by half-lines c and d). Here, and throughout the paper all operations on numbers associated with SVm relations are taken modulo m.

Example 1. ACSP(SV8) instance v1[[6]]v2∧v2[[0]]v1 is satisfiable as v1 and v2 can be instantiated with A and B as shown in Fig. 2a.

Example 2. A CSP(SV8) instance ∧i,j∈{1,2,3},i̸=j vi[[1]]vj cannot be satisfiable, because all three interior angles of the triangle which is spanned by v1, v2, v3 are constrained to be less than 45◦ by the atomic relation [[1]]. This contradicts the fact that the interior angles of a triangle add up to 180◦ .

4 NP-Hardness of CSP(SV2)

In this section we show that deciding CSP(SV2) is NP-hard. The NP-hardness result suggests that developing an algorithm parametrized with m that decides CSP(SVm) in polynomialtime for all m is not possible.

For our proof we use a reduction from the BETWEENNESS problem, originally introduced as total ordering problem [Opatrny, 1979]. In BETWEENNESS we are given a set of constraints in the form B(qi, qj, qk), i, j, k ∈ {1, . . . , n} where qi, qj , qk are variables that range over the set of rational numbers Q. A constraint B(qi, qj, qk) stands for (qi < qj < qk) ∨ (qi > qj > qk), stating that "qj is between qi and qk". Deciding whether there exists a valuation satisfying all BETWEENNESS constraints is NP-complete [Opatrny, 1979].

Theorem 3. CSP(SV2) is NP-hard.

Proof sketch. Given an instance χ of BETWEENNESS over n variables. We translate the BETWEENNESS constraints to CSP(SV2) constraints. First, for every variable qj occurring in a BETWEENNESS constraint we introduce a variable v1 j in SV2. If a variable qj occurs tj times as the second argument of a BETWEENNESS constraint we additionally introduce one new variable v2 j , v3 j , . . . , vtj j in SV2 for every occurrence. We tie together all v1 j , v2 j , . . . , vtj j by introducing constraints vℓ j Svℓ+1 j for all 1 ≤ ℓ ≤ tj - 1. Thus, we ensure that the points are co-located but possibly equipped with different orientations from Θ2 = {0◦ , 180◦}. For every constraint B(qi, qj, qk) in χ we introduce two SV2 constraints, v1 i [[1]]vℓ j ∧ vℓ j [[1]]v1 k , with ℓ being the ℓth appearance of qj as second argument. All other variables are related via the universal relation to each other. Finally, we obtain a CSP(SV2) instance φ involving only atomic relations and the universal relation, where the BETWEENNESS to CSP(SV2) reduction is done in polynomial time in the number of variables.

We need to show that φ is satisfiable if and only if χ has a solution. First, assume χ is satisfiable. Then there exists a valuation function f that assigns to each variable qj a point in Q, such that all BETWEENNES constraints are satisfied. Then, by assigning (0, f(qj), θℓ j ) ∈ R2 × Θ2 to each vℓ j we obtain a valuation that satisfies each constraint v1 i [[1]]vℓ j ∧ vℓ j [[1]]v1 k , where we choose θℓ j = 0◦ if f(qi) < f(qj) < f(qk) and θℓ j = 180◦ if f(qk) < f(qj) < f(qi).

Let us now consider φ is satisfiable. Then there is a valuation function that assigns to each variable vℓ j a value (xj , yj , θℓ j ) ∈ R2 ×Θ2, such that v1 i [[1]]vℓ j ∧ vℓ j [[1]]v1 k is satisfied. Wlog. we can assume that all xj are zero, and all yj rational, because a solution for φ is invariant under projection to the y-axis and a sufficiently small perturbation of yj . Then by assigning to each qj a rational number yj for j = 1, . . . , n we obtain a solution for χ

5 The NP-Membership of CSP(SVm)

In this section we give a decision procedure for SVm. This NP-membership proof establishes a connection to the problem of solving a system of linear inequalities which we later utilize to develop the practical decision procedure.

The following lemma from vector algebra establishes a connection between the determinant of two vectors in R2 and their relative directions. Recall that the determinant of a 2by-2 matrix is defined as

Lemma 4. Let two vectors ⃗v, ⃗w ∈ R2 be given and let (⃗v, ⃗w) be a 2×2 matrix having ⃗v and ⃗w as its column vectors. Then ⃗w is to the left (right) of ⃗v, if and only if the determinant of two vectors, i.e, det(⃗v, ⃗w), is greater (less) than 0. Vector ⃗w is parallel to ⃗v, if and only if det(⃗v, ⃗w) = 0.

Convex SVm relations play an important role in the algorithm presented in the next section. We say that an SVm relation [[c..d]] is convex, if for a given SVm object A the sector of A that relation [[c..d]] describes is convex (i.e., the central angle of the sector is less or equals 180◦ ). This is the case if and only if mod(d - c, m) ≤ m/2. Any atomic relation is for example convex. In SV8 (cf. Figure 2a) relation [[5..1]] is convex. By contrast, relation [[5..2]] is not convex, because the union of sectors 5 to 2 in counterclockwise order span 225◦ .

Lemma 5. A constraint v1[[c..d]]v2 with a convex relation [[c..d]] can be formulated as a conjunction of nonlinear inequalities.

Proof. Let ⃗v = (x2, y2) - (x1, y1) ∈ R2 be a vector with initial point (x1, y1) and terminal point (x2, y2), where (x1, y1) and (x2, y2) are the positions of variables v1 and v2 in R2 , respectively. Let u(v1, s) be a unit vector having the same orientation as half-line s of variable v1, i.e., u(v1, s) = (cos(θ1+s 360◦ m ), sin(θ1+s 360◦ m )), where θ1 is the orientation component of v1. Then constraint v1[[s]]v2 is satisfiable, if and only if ⃗v is to the left of or parallel to u(v1, c) and ⃗v is to the right of u(v1, d), i.e., by Lemma 4

By expanding the determinant expression according to (2) we obtain a conjunction of two inequalities which are linear in x1, x2, y1, y2 and nonlinear in θ1.

Theorem 6. CSP(SVm) is in NP.

Proof. An NP algorithm for CSP(SVm) is obtained by nondeterministically choosing the atomic relations and values for the orientations of the input formula φ, and translating each conjunct of φ to inequalities by Lemma 5. These inequalities are all linear as the non-linear parts containing θi are already instantiated, and can be solved in polynomial time by [Schrijver, 1986].

6 A Practical Algorithm for CSP(SVm)

The decision procedure in Theorem 6 is not yet practical as it non-deterministically and non-systematically selects values for orientation variables θ1, . . . , θn. In this section we present an improved algorithm that searches for the values of the orientation variables in a systematic manner. The algorithm decides CSP(SVm) and returns a model of the input formula for all m = 2r where r is a positive integer.

The idea behind the algorithm is based on the following four observations:

1. If we fix orientations θ1, . . . , θn of all variables v1, . . . , vn of an atomic CSP(SVm) instance φ, then φ can be solved in polynomial time. However, there are mn possible choices for fixing the orientations.
2. To overcome this exponential complexity in searching for the orientations we use a duality between the uncertainty about the orientation and the uncertainty about the direction relation. The next example illustrates this duality.

Example 7. An atomic constraint vi[[1]]vj where the orientation of vi is restricted to {135◦ , 180◦ , 225◦} (see Figure 3a) is satisfiable if and only if constraint vi[[4..7]]vj is satisfiable where the orientation of vi is fixed to 0◦ (see Figure 3b). Here, the uncertainty about the orientation (i.e., {135◦ , 180◦ , 225◦}) is transferred to the uncertainty of the direction relation (i.e., [[4..7]]). Though solving both constraints is equivalent, the latter can be solved more efficiently, because we do not have to search for the orientations, and convex relations like [[4..7]] allow for efficient reasoning.

1. By using this duality we can solve a weaker problem efficiently. Parameters that do not even satisfy the weaker problem can therefore be pruned.
2. By using the weaker problem a binary search with pruning can be realized that recursively restricts the domain of orientation variables until a model is found or unsatisfiability is shown.

The four observations are employed in algorithm DECIDESTARVARS (Algorithm 1) which has SEARCH (Algorithm 2) as a subroutine. In what follows, for two variables vi = (xi, yi, θi) and vj = (xj, yj, θj) we will use notations vi Rij vj and Rij (xi, yi, xj , yj , θi) interchangeably to denote an SVm constraint. Note that the orientation variable θj is omitted in Rij(xi, yi, xj, yj, θi), as an SVm relation is not dependent on the orientation of the second variable.

Algorithm 1: DECIDESTARVARS(φ, m, n) Input: A CSP(SVm) instance φ = ∧i̸=j Rij(xi, yi, xj, yj, θi), granularity m = 2r (r ∈ N), and number n of variables. Output: If φ is satisfiable, then a model is returned. Otherwise, fail is returned.

1 begin 2 for each Rij in φ do 3 Choose an atomic relation [[sij ]] ∈ R such that [[sij]] ⊂ Rij. Then substitute [[sij]] for Rij in formula φ. 4 ψ ←φ 5 for each conjunct [[sij ]](xi, yi, xj , yj , θi) in ψ do 6 Substitute θij for θi. 7 return SEARCH(ψ,m, n,Θm|m0 , . . . ,Θm|m0 )

We now detail the algorithm: On input φ,m, n algorithm DECIDESTARVARS first makes φ atomic by picking an atomic relation for each relation in φ non-deterministically (lines 2-3). In a deterministic variant this procedure can be realized with a backtracking search.

To enable pruning of the parameter space with the duality property previously mentioned, a new formula ψ is generated by substituting θij for θi (lines 4-6). Then formula ψ is passed to the subroutine SEARCH, which systematically searches for the values for θij. The notation dom(θij) = Θm|ba is used to denote a reduced parameter space of the values for θij, where dom(θij) stands for the domain of θij and

Algorithm 2: SEARCH(ψ, m, n, Θm|b1 a1 , . . . , Θm|bn an )

Input: An atomic formula

ψ = ∧i̸=j [[sij ]](xi, yi, xj , yj , θij ), granularity m = 2r (r ∈ N), number n of variables, and domain restrictions Θm|bi ai for i = 1, . . . , n.

Output: If ψ satisfiable with dom(θij) = Θm|bi ai for i, j = 1, . . . , n, i ̸= j, then a model of ψ is returned. Otherwise, fail is returned.

1 begin 2 for i ← 1 to n do 3 Θm|bi ai ←CHOOSE(Θm|(ai+bi)/2 ai , Θm|bi (ai+bi)/2) 4 if ψ has a model with dom(θij ) = Θm|bi ai then 5 if bi - ai = 1 for i = 1, . . . , n then 6 return a model of ψ 7 return SEARCH(ψ, m, n, Θm|b1 a1 , . . . , Θm|bn an ) 8 return fail

For example the orientations values {135◦ , 180◦ , 225◦ } in Example 7 is given by Θ8|64 . We note that Θm|m0 is the complete orientation domain Θm.

For brevity of presentation SEARCH is realized in a nondeterministic way using selection (CHOOSE, line 3) and failure (fail, line 8). CHOOSE will always return the correct halves of Θm|bi ai , i = 1, . . . , n for which the input formula ψ is satisfiable (line 4). If these do not exist, the algorithm will terminate and return fail. The satisfiability check in line 4 prunes the search space in the deterministic variant of algorithm SEARCH. In what follows we prove that this can be done in polynomial time by applying the duality property and solving a conjunction of linear inequalities.

As already observed in Example 7, there is a duality between the uncertainty about orientations and the uncertainty about direction relations, i.e., the disjunction of sectors in Figure 3a is equal to the sector in Figure 3b. In general, the following duality equation holds for two oriented points A = (x1, y1, θ1) and B = (x2, y2, θ2) with fixed position (x1, y1) of A:

Theorem 8. Finding a model of formula ψ := ∧i̸=j [[sij]](xi, yi, xj, yj, θij), where each θij is restricted to Θm|bi ai with bi - ai ≤ m/2, i, j = 1, . . . , n, i ̸= j, can be done in polynomial time.

Proof sketch. We first show that the satisfiability of the stated problem is equivalent to the satisfiability of formula ψ′ := ∧i̸=j [[sij +ai ..sij +bi]](xi, yi, xj , yj , 0◦ ):

The first equality is due the fact that each θij appears in exactly one conjunct and can therefore be pulled into the conjunction. The second equality follows from equation (3). Now we show that ψ′ is solvable in polynomial time. Solving ψ′ is equivalent to solving a conjunction of inequalities, because all relations in ψ′ are convex (bi - ai ≤ m/2) such that each conjunct of ψ′ can be translated to inequalities by Lemma 5. These inequalities are all linear as the non-linear parts containing θi evaluate to constants, and can be solved in polynomial time by [Schrijver, 1986].

Corollary 9. The satisfiability check in line 4 of Algorithm 2 can be done in polynomial time.

Now we prove that DECIDESTARVARS is sound and complete. The next lemma states that satisfiability of ψ is a weaker problem, i.e., a necessary condition for satisfiability of the input formula φ.

Lemma 10. Let φ := ∧i̸=j [[sij]](xi, yi, xj, yj, θi) and ψ := ∧i̸=j [[sij]](xi, yi, xj, yj, θij) be two formulas with dom(θi) = dom(θij) = Θm|bi ai for i, j = 1, . . . , n, i ̸= j. Then φ is satisfiable only if ψ is satisfiable.

Proof. Let a model M of φ be given. Then we vacuously obtain a model of ψ which is same as M except for the fact that the valuation of θi is extended to θij.

After some recursive application of SEARCH each restricted orientation domain Θm|bi ai consists of only one element. Then a model of ψ induces a model of φ:

Lemma 11. Let φ and ψ be defined as in Lemma 10. If all Θm|bi ai consists of only one element, i.e., bi - ai = 1 for i = 1, . . . , n, then φ is satisfiable if ψ is satisfiable and a model of ψ can be identified with a model of φ.

Proof. Because Θm|bi ai consists of only one element, say ti, all θij for all j = 1, . . . , n are evaluated to the same value ti. Thus, given a model of ψ, the assignment of the value ti to θi while preserving the values for xi, yi for each i, yields a model of φ.

Theorem 12. DECIDESTARVARS is a sound and complete algorithm.

Proof. For the soundness assume that on input φ, m and n DECIDESTARVARS returns a model. Then, according to line 5-6 in Algorithm 2, ψ is satisfiable with dom(θij) = Θm|bi ai with bi - ai = 1 for i = 1, . . . , n. Then by applying Lemma 11 we obtain a model of φ.

For the completeness assume that DECIDESTARVARS returns fail. Then ψ is not satisfiable, because SEARCH implements a complete search for finding the values for θij such that there is a model of ψ. It follows that φ is not satisfiable by Lemma 10.

7 Evaluation

We evaluated DECIDESTARVARS for 100 random atomic CSP(SVm) instances with varying m and n, and have recorded the average computing time in seconds (the variance is shown in parentheses). For solving systems of linear inequalities we used function linprog from the MATLAB Optimization Toolbox. The evaluation was done on a machine with Intel R© Core TM 2 E6700 CPU and 4 GB RAM.

From the table we conclude that the increase of computing time in the size of granularity m is only logarithmic in average case. This efficiency, which is obtained by the pruning step integrated in the algorithm, can be utilized to approximate relative directions with a high resolution.

However, as the algorithmic complexity suggests, the computing time increases exponentially in the number n of variables. Thus, the proposed algorithm is suitable for applications which allow for precomputation or which involve only a limited number of objects.

8 Application Example

Mossakowski and Moratz [2012] present representation of navigation regulations as a relevant application domain for directional calculi. We pick up the example from this paper which is set in the context of sea navigation. Maritime traffic regulations issued by the International Maritime Organization (IMO) comprise the following rule:

When two sailing vessels are approaching one another, as to involve the risk of collision, one of them shall keep out of the way of the other as follows: (i) when each has the wind on a different side, the vessel which has the wind on the port side shall keep out of the way of the other. (Rule 12 i, IMO)

See Figure 4a for an illustration of the rule in which vessel G has to give way and vessel K has to keep course, using the common avoidance behavior of turning away from the vessel that has right of way. Vessel G aims to pass behind the stern of vessel K, thus turning towards it. Considering rule and avoidance pattern are stated for exactly two vessels, an important question is: does this rule also handle a 3-ship encounter? Or can it lead to contradicting recommendations? To answer this question we model the rule in SV8, mapping natural language terms to qualitative spatial relations as shown in Figure 4b. Assuming the same wind direction for both vessels, we obtain the following conjunction of qualitative relations:

Additionally, vessel G should give way by turning to starboard, if vessel K approaches from starboard, and turning to port, otherwise. We can thus describe the situations that lead to mutually exclusive turning actions by formulas α and β:

To answer our question about a 3-ship encounter we construct a CSP with variables for vessels A, B, C and wind W:

If formula (4) is satisfiable, then there exists a configuration that requires two mutually exclusive commands to be carried out and the rule is known to not generalize to 3-ship encounters. Our sound decision method determines satisfiability of formula (4) and it outputs a configuration from which we generated Figure 4c, showing a conflict for vessel C.

One could approach the task with constraint propagation using relation composition as suggested by [Mossakowski andMoratz, 2012]. This outputs, however, false-positives and cannot compute a realization. Thus one has to check each output manually which is an infeasible task. Our reasoning method is thus the superior approach to the task. For more information on the application of StarVars in the sea navigation domain we refer to [Kreutzmann et al., 2013].

9 Summary and Conclusions

We have developed a spatial representation, StarVars, which augments cardinal direction relations to represent relative directional knowledge. By introducing orientation variables we are able to apply computationally cheaper decision procedures for cardinal directions to the hard problem of handling directional knowledge. We gave an NP decision procedure for StarVars, and therefore it can replace existing directional relation languages for which no effective decision procedures are available today. Additionally, our algorithm can determine a model of consistent CSP instances, which is valuable for many applications that require a visual presentation.

Future works aims to improve our decision procedure, in particular to counter-act the exponential growth with respect to the number of variables using heuristics.

Acknowledgements

The authors thank the anonymous reviewers for helpful feedback. Financial support by DFG (SFB/TR 8 Spatial Cognition, project R3-[Q-Shape]) is acknowledged.