Several studies in Qualitative Spatial and Temporal Reasoningdiscuss translations of the satisfiability problem on qualitativeconstraint languages into propositional SAT. Most of these encodings focus on compactness, while propagation strength is seldom discussed. In this work, we focus on temporal reasoning with the Point Algebra and Allen's Interval Algebra. We understand all encodings as a combination of propagation andsearch. We first give a systematic analysis of existing propagation approachesfor these constraint languages. They are studied and ordered with respect to their propagation strengthand refutation completeness for classes of input instances. Secondly, we discuss how existing encodings can be derived fromsuch propagation approaches. We conclude our work with an empirical evaluation which shows that theolder ORD-encoding by Nebel and Bürckert performs better than more recently suggested encodings.

Qualitative spatial and temporal reasoning is a research field that studies relational, constraint-based formalisms for representing, and reasoning about, spatial and temporal information. The standard approach for checking consistency is based on an exhaustive representation of possible configurations between three entities, the so-called composition tables. These tables, however, encode semantic background knowledge in a redundant way, which becomes a size and efficiency issue, when the composition table needs to be grounded as done in SAT encodings of problem instances. % In this paper, we present a new framework that allows for decomposing composition tables into logically simpler parts, while preserving logical equivalence, e.g., the decomposition in start- and end-points for Allen's Interval Calculus. We show that finding such decompositions is an NP-complete problem and present a SAT-based method to generate decompositions. Finally, we discuss the impact of our decomposition method on SAT encodings of problem instances, and present a reasoning system built on decompositions that compares favorably with state-of-the-art solvers.

We construct an homogeneous (and ω-categorical) representation of the relation algebra RCC8, which is one of the fundamental formalisms for spatial reasoning. As a consequence we obtain that the network consistency problem for RCC8 can be solved in polynomial time for networks of bounded treewidth.

The generation of route descriptions is a fundamental task of navigation systems. A particular problem in this context is to identify routes that can easily be described and processed by users. In this work, we present a framework for representing route n

Route navigation is one of the most widely used everyday application of spatial data. In this paper we investigate how a qualitative representation of route networks can be derived from map data and how this representation can be used to reason about route descriptions. We introduce a concept of route graph that provides an abstract layer on top of metric map data and thus allows for a compact representation of route information. We present selected queries and reasoning tasks that can be expressed in this abstraction layer.

This paper introduces restart and nogood recording techniques in the domain of qualitative spatial and temporal reasoning. Nogoods and restarts can be applied orthogonally to usual methods for solving qualitative constraint satisfaction problems. In particular, we propose a more general definition of nogoods that allows for exploiting information about nogoods and tractable subclasses during backtracking search. First evaluations of the proposed techniques show promising results.