Une approche SAT incrémentale pour raisonner efficacement sur les réseaux de contraintes qualitatives

International audienceLe langage RCC8 est un formalisme largement utilisé pour décrire des arrangements topologiques de régions dans l'espace. Deux problèmes fondamentaux sont asso-ciés au langage RCC8 : la satisfiabilité et la réalisation. Soit un réseau de contraintes qualitatives (QCN) de RCC8, le problème de satisfiabilité est de décider s'il est possible d'assigner des régions aux variables du QCN de telle sorte que les contraintes soient satisfaites (solution). Le problème de réalisation est le fait de produire un modèle spatial qui peut servir de solution. Dans cet article, nous combinons les deux lignes de recherches mentionnés au-dessus et nous explorons l'idée de relier le problème de satisfiabilité et de réalisation. Nous nous limitons aux QCN qui, quand ils sont satisfiables, sont réalisables avec des rectangles. En effet, nous proposons une approche SAT in-crémentale afin d'être capable de raisonner sur le langage RCC8 en nous laissant guider par les contre-exemples. Nous avons expérimentalement évalué notre approche et étudié ses performances face aux solveurs de l'état de l'art pour raisonner en RCC8 en utilisant de nombreux ensembles d'instances. Notre approche tient la charge et est compétitive face aux solveurs de l'état de l'art sur les instances considérées. Abstract The RCC8 language is a widely-studied formalism for describing topological arrangements of spatial regions. Two 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 ⇤ Papier doctorant : Gaël Glorian 1 est auteur principal. realization problem is producing an actual spatial model that can serve as a solution. In 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. We restrict ourselves to QCNs that, when satisfiable, are realizable with rectangles. In particular, we propose an incremental SAT-based approach for providing a framework that reasons about the RCC8 language in a counterexample-guided manner. We 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