Reasoning about Space and Change with Answer Set Programming Modulo Theories

1 Introduction

The key requirements in a number of dynamic spatial domains (such as robotics or architecture design) are to perform non-monotonic and conterfactual reasoning, enable explanation and diagnosis as well as belief revision about spatial objects and their change in time. Additionally, tasks like causal explanation and default reasoning often need to be considered mutually with spatial consistency. The abovementioned features are necessary in scenarios where spatial configuration of objects undergo a change as a result of interactions with physical environment while the agents possess incomplete or uncertain knowledge and need to perform spatial reasoning and planning. A number of domain-independent approaches for modelling spatial change have been developed, e.g., Shanahan [Shanahan, 1995] integrated a first-order theory of shape with the situation calculus for describing common-sense laws of motion, whereas Bhatt and Loke [Bhatt and Loke, 2008] presented a framework for modelling dynamic spatial systems by integrating qualitative spatial theories into the situation calculus. Nevertheless, no systems currently exist that are capable of efficient and general nonmonotonic spatial reasoning for dynamic domains.

2 Qualitative Space in ASPMT

The joint work with M. Bhatt and C. Schultz accomplished so far amounts to devising the so called ASPMT(QS) framework for spatio-temporal reasoning under stable models semantics [Wał˛ega et al., 2015]. Our approach is based on Answer Set Programming Modulo Theories (ASPMT) paradigm extended to spatial and spatio-temporal domains. Spatial reasoning is performed in an analytic manner, i.e., the relations are encoded as polynomial constraints. The main reasoning task -determining whether a spatial configuration is consistent- is equivalent to determining whether a particular system of polynomial constraints is satisfiable. The reasoning method uses Satisfiability Modulo Theories (SMT) with real nonlinear arithmetic, and can be performed in a sound and complete manner.

Conceptual Parametrics: Integrated Framework Our implementation of ASPMT(QS) 1 is built on top of ASPMT2SMT [Bartholomew and Lee, 2014] - a compiler that translates a tight fragment of ASPMT into SMT instances. Then Z3 - an off the shelf SMT solver is used to compute spatially consistent answer sets. Recently, we have extended the approach as presented in Figure. 1. Now, a consistent spatial configuration is also generated (quantification), and the qualitative constraints corresponding to a particular answer set are encoded as geometric constraints in order to construct a 2D parametric diagram: spatial objects in the diagram can be manipulated (scaled, rotated, translated) and in response the geometric solver modifies other spatial objects to ensure that the qualitative spatial constraints are always satisfied. The finalised parametric diagram is sent to a polyhedra op-

1 A prototypical implementation of the system is available online publicly from Docker Hub, a cloud-based registry service for building and shipping applications: https://hub.docker.com/r/ spatialreasoning/aspmtqs/. It contains the core system, minimal working examples, short description and installation instructions.

c

c

pa

p pb

ca

pa pb erator module based on a mapping between the abstract spatial model and the 3D polyhedral model. The operator module is equipped with a set of primitive polyhedra operators that are employed to transform the 3D model according to the mapped abstract qualitative model. Every (spatially consistent) answer set is thus used to generate a qualitatively distinct 3D model.

Since ASPMT(QS) uses polynomial encodings of spatial relations it has a great expressiveness; it is able to express a number of relations from the well-known qualitative spatial reasoning approaches. The following Proposition 1 has been proved in [Wał˛ega et al., 2015].

Proposition 1. Each relation of Interval Algebra, Rectangle Algebra, Left-Right Algebra, Region Connection Calculus-5 in the domain of convex polygons with a finite number of vertices and Cardinal Direction Calculus may be expressed in ASPMT(QS).

In what follows we give examples of reasoning tasks that may be performed in the framework.

Euclid Constructions. ASPMT(QS) enables to perform, famous Euclid constructions such as bisecting an angle (Proposition 9, Book 1) by means of a 'ruler and compass method'. Given three distinct points p↪ pa↪ pb such that pa↪ pb are equidistant to p, the task is to bisect the angle formed by the points. The famous Euclid method consist of constructing circles ca and cb and a point pc coincident to them (Figure 2). The claim is that the segment from p to pc bisects the angle. p pb pa c

pc pc ASPMT(QS) enables to check if the construction is: (i) consistent, i.e., if the constructed segment bisects the angle, and (ii) sufficient, i.e., if the method always leads to the construction of a segment bisecting the angle.

cb Architecture Design. ASPMT(QS) can be combined with Computer Aided Design systems (e.g., FreeCAD) in order to determine qualitatively consistent relations, and instantiate them by creating an architectural design. As a result ASPMT(QS) may be used in the early-phase conceptual design of buildings. Given a set of constraints the system enables to compute a spatial graph (i.e., desired qualitative relations between areas of the building) and its instantiation, i.e., a complete floor plant layout (Figure 3).

Spatio-Temporal Histories. ASPMT(QS) is capable of handling space-time histories, i.e., regions with both spatial and temporal components and their mutual interactions. Consider a scenario (Figure 4) in which a robot with a limited range of motion is asked to get the cup of coffee without hitting the laptop or the risk of spilling the coffee on in.

c

f1(H3)

f1(H4)

ca

pa Figure 4: ASMPT(QS) solution to the manipulation task.

cb p pb ASPMT(QS) enables to plan robot's movements and check that all required relations between spatio-temporal objects (hand, laptop and coffee) are satisfied.

3 FutureWork

The future work consists of further development of the framework, in particular optimising the encodings in order to be able to perform more complex spatio-temporal reasoning. Furthermore the system will be applied to practical problems, such as navigation of mobile robots and dynamic geographic information systems.

Acknowledgements

The author is supported by the Polish National Science Centre grant DEC-2011/02/A/HS1/00395.