An Automatic Decomposition Method for Qualitative Spatial and Temporal Reasoning

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.