Abstract
The \({\mathcal {RCC}}8 \) language is a widely-studied formalism for describing topological arrangements of spatial regions. Two fundamental reasoning problems that are associated with \({\mathcal {RCC}}8 \) are the problems of satisfiability and realization. Given a qualitative constraint network (QCN) of \({\mathcal {RCC}}8 \), 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. Researchers in \({\mathcal {RCC}}8 \) 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. 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 \(\mathrm {SAT}\)-based approach for providing a framework that reasons about the \({\mathcal {RCC}}8 \) language in a counterexample-guided manner. The incrementality of our approach also avoids the usual blow-up and the lack of scalability in \(\mathrm {SAT}\)-based encodings. Specifically, our \(\mathrm {SAT}\)-translation is parsimonious, i.e, constraints are added incrementally in a manner that guides the embedded \(\mathrm {SAT}\)-solver and forbids it to find the same counter-example twice. We experimentally evaluated our approach and studied its scalability against state-of-the-art solvers for reasoning about \({\mathcal {RCC}}8 \) relations using a varied dataset of instances. The approach scales up and is competitive with the state of the art for the considered benchmarks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
\(\mathring{A}\) denotes the interior of A.
- 2.
The name comes from the historical figure who used to also do a lot of \({\text {CEGAR}}\).
- 3.
The generator comes with the \(\mathrm {Renz}\text {-}\mathrm {Nebel01} \) solver.
References
Sioutis, M., Alirezaie, M., Renoux, J., Loutfi, A.: Towards a synergy of qualitative spatio-temporal reasoning and smart environments for assisting the elderly at home. In: IJCAI Workshop on Qualitative Reasoning (2017)
Bhatt, M., Guesgen, H., Wölfl, S., Hazarika, S.: Qualitative spatial and temporal reasoning: emerging applications, trends, and directions. Spat. Cogn. Comput. 11, 1–14 (2011)
Dubba, K.S.R., Cohn, A.G., Hogg, D.C., Bhatt, M., Dylla, F.: Learning relational event models from video. J. Artif. Intell. Res. 53, 41–90 (2015)
Story, P.A., Worboys, M.F.: A design support environment for spatio-temporal database applications. In: Frank, A.U., Kuhn, W. (eds.) COSIT 1995. LNCS, vol. 988, pp. 413–430. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60392-1_27
Randell, D.A., Cui, Z., Cohn, A.: A spatial logic based on regions and connection. In: KR (1992)
Bouzy, B.: Les concepts spatiaux dans la programmation du go. Revue d’Intelligence Artificielle 15, 143–172 (2001)
Lattner, A.D., Timm, I.J., Lorenz, M., Herzog, O.: Knowledge-based risk assessment for intelligent vehicles. In: KIMAS (2005)
Heintz, F., de Leng, D.: Spatio-temporal stream reasoning with incomplete spatial information. In: ECAI (2014)
Randell, D.A., Galton, A., Fouad, S., Mehanna, H., Landini, G.: Mereotopological correction of segmentation errors in histological imaging. J. Imaging 3(4), 63 (2017)
Renz, J., Nebel, B.: On the complexity of qualitative spatial reasoning: a maximal tractable fragment of the region connection calculus. Artif. Intell. 108(1–2), 69–123 (1999)
Li, S.: On topological consistency and realization. Constraints 11, 31–51 (2006)
Renz, J., Nebel, B.: Qualitative spatial reasoning using constraint calculi. In: Aiello, M., Pratt-Hartmann, I., Van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 161–215. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5587-4_4
Golumbic, M.C., Shamir, R.: Complexity and algorithms for reasoning about time: a graph-theoretic approach. J. ACM 40, 1108–1133 (1993)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Huang, J., Li, J.J., Renz, J.: Decomposition and tractability in qualitative spatial and temporal reasoning. Artif. Intell. 195, 140–164 (2013)
Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol. 5717, pp. 304–311. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04772-5_40
Seipp, J., Helmert, M.: Counterexample-guided cartesian abstraction refinement. In: Borrajo, D., et al. (eds.) Proceedings of ICAPS 2013. AAAI (2013)
Soh, T., Le Berre, D., Roussel, S., Banbara, M., Tamura, N.: Incremental SAT-based method with native boolean cardinality handling for the hamiltonian cycle problem. In: Fermé, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 684–693. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11558-0_52
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–24 (2016)
Pulina, L.: The ninth QBF solvers evaluation - preliminary report. In: Lonsing, F., Seidl, M. (eds.) Proceedings of QBF@SAT 2016, CEUR Workshop Proceedings, vol. 1719. CEUR-WS.org (2016)
Hooker, J.N.: Logic-based methods for optimization. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 336–349. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58601-6_111
Chu, Y., Xia, Q.: A hybrid algorithm for a class of resource constrained scheduling problems. In: Barták, R., Milano, M. (eds.) CPAIOR 2005. LNCS, vol. 3524, pp. 110–124. Springer, Heidelberg (2005). https://doi.org/10.1007/11493853_10
Hooker, J.N.: A hybrid method for the planning and scheduling. Constraints 10(4), 385–401 (2005)
Tran, T.T., Beck, J.C.: Logic-based benders decomposition for alternative resource scheduling with sequence dependent setups. In: Proceedings of ECAI 2012 (2012)
de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438–455. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45620-1_35
Ji, X., Ma, F.: An efficient lazy SMT solver for nonlinear numerical constraints. In: Proceedings of WETICE 2012 (2012)
Renz, J.: A canonical model of the region connection calculus. JANCL 12, 469–494 (2002)
Renz, J., Ligozat, G.: Weak composition for qualitative spatial and temporal reasoning. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 534–548. Springer, Heidelberg (2005). https://doi.org/10.1007/11564751_40
Li, S., Ying, M.: Region connection calculus: its models and composition table. Artif. Intell. 145, 121–146 (2003)
Long, Z., Schockaert, S., Li, S.: Encoding large RCC8 scenarios using rectangular pseudo-solutions. In: Proceedings of KR 2016 (2016)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning, pp. 466–483. Springer, Heidelberg (1983). https://doi.org/10.1007/978-3-642-81955-1_28
Lagniez, J.M., Le Berre, D., de Lima, T., Montmirail, V.: A recursive shortcut for CEGAR: application to the modal logic K satisfiability problem. In: Proceedings of IJCAI 2017 (2017)
Long, Z.: Qualitative spatial and temporal representation and reasoning: efficiency in time and space. Ph.D. thesis, Faculty of Engineering and Information Technology, University of Technology Sydney (UTS), January 2017
Savicky, P., Vomlel, J.: Triangulation heuristics for BN2O networks. In: Sossai, C., Chemello, G. (eds.) ECSQARU 2009. LNCS (LNAI), vol. 5590, pp. 566–577. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02906-6_49
Sioutis, M., Koubarakis, M.: Consistency of chordal RCC-8 networks. In: Proceedings of ICTAI 2012. IEEE Computer Society (2012)
Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell. 49(1–3), 61–95 (1991)
Long, Z., Sioutis, M., Li, S.: Efficient path consistency algorithm for large qualitative constraint networks. In: Proceedings of IJCAI 2016 (2016)
Sioutis, M., Long, Z., Li, S.: Leveraging variable elimination for efficiently reasoning about qualitative constraints. Int. J. Artif. Intell. Tools (2018, in press)
Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_23
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Westphal, M., Wölfl, S., Gantner, Z.: GQR: a fast solver for binary qualitative constraint networks. In: Proceedings of the AAAI Spring Symposium. AAAI (2009)
Renz, J., Nebel, B.: Efficient methods for qualitative spatial reasoning. J. Artif. Intell. Res. 15, 289–318 (2001)
Sioutis, M., Condotta, J.-F.: Tackling large qualitative spatial networks of scale-free-like structure. In: Likas, A., Blekas, K., Kalles, D. (eds.) SETN 2014. LNCS (LNAI), vol. 8445, pp. 178–191. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07064-3_15
Sioutis, M., Condotta, J., Koubarakis, M.: An efficient approach for tackling large real world qualitative spatial networks. Int. J. Artif. Intell. Tools 25, 1–33 (2016)
Barabási, A.L., Albert, R.: Emergence of scaling in random networks. Science 286(5439), 509–512 (1999)
Acknowledgments
The authors would like to thank the anonymous reviewers for their insightful comments. Part of this work was supported by the French Ministry for Higher Education and Research, the Haut-de-France Regional Council through the “Contrat de Plan État Région (CPER) DATA” and an EC FEDER grant.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Glorian, G., Lagniez, JM., Montmirail, V., Sioutis, M. (2018). An Incremental SAT-Based Approach to Reason Efficiently on Qualitative Constraint Networks. In: Hooker, J. (eds) Principles and Practice of Constraint Programming. CP 2018. Lecture Notes in Computer Science(), vol 11008. Springer, Cham. https://doi.org/10.1007/978-3-319-98334-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-98334-9_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98333-2
Online ISBN: 978-3-319-98334-9
eBook Packages: Computer ScienceComputer Science (R0)