An Incremental SAT-Based Approach to Reason Efficiently On Qualitative Constraint Network

International audienceThe RCC8 language is a widely-studied formalism for describing topological arrangements of spatial regions.\r\nTwo fundamental reasoning problems that are associated with RCC8 are the problems of satisfiability and realization. Given a qualitative constraint network (QCN) of RCC8, the satisfiability problem is deciding whether it is possible to assign regions to the spatial variables of the QCN in such a way that all of its constraints are satisfied (solution). The realization problem is producing an actual spatial model that can serve as a solution.\r\n\r\nResearchers in RCC8 focus either on symbolically checking the satisfiability of a QCN or on presenting a method to realize (valuate) a satisfiable QCN. To the best of our knowledge, a combination of those two lines of research has not been considered in the literature in a unified and homogeneous approach, as the first line deals with native constraint-based methods, and the second one with rich mathematical structures that are difficult to implement.\r\n\r\nIn this article, we combine the two aforementioned lines of research and explore the opportunities that surface by interrelating the corresponding reasoning problems, viz., the problems of satisfiability and realization. In particular, we propose an incremental SAT-based approach for providing a framework that reasons about the RCC8 language in a counterexample-guided manner.\r\n\r\nThe incrementality of our approach also avoids the usual blow-up and the lack of scalability in SAT-based encodings.\r\nSpecifically, our SAT-translation is parsimonious, i.e, constraints are added incrementally in a manner that guides the embedded SAT-solver and forbids it to find the same counter-example twice.\r\n\r\nWe experimentally evaluated our approach and studied its scalability against state-of-the-art solvers for reasoning about RCC8 relations using a varied dataset of instances. The approach scales up and is competitive with the state of the art for the considered benchmarks