Hostname: page-component-cd9895bd7-lnqnp Total loading time: 0 Render date: 2024-12-25T05:30:17.886Z Has data issue: false hasContentIssue false
  • English
  • Français

Modular Constraint Solver Cooperation via Abstract Interpretation

Published online by Cambridge University Press:  22 September 2020

PIERRE TALBOT Open the ORCID record for PIERRE TALBOT [Opens in a new window] ,
ÉRIC MONFROY  and
CHARLOTTE TRUCHET
PIERRE TALBOT
Affiliation:
Interdisciplinary Centre for Security, Reliability and Trust (SNT), University of Luxembourg, Esch-sur-Alzette, Luxembourg (e-mail: [email protected])
ÉRIC MONFROY
Affiliation:
University of Angers, Angers, France (e-mail: [email protected])
CHARLOTTE TRUCHET
Affiliation:
University of Nantes, Nantes, France (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Cooperation among constraint solvers is difficult because different solving paradigms have different theoretical foundations. Recent works have shown that abstract interpretation can provide a unifying theory for various constraint solvers. In particular, it relies on abstract domains which capture constraint languages as ordered structures. The key insight of this paper is viewing cooperation schemes as abstract domains combinations. We propose a modular framework in which solvers and cooperation schemes can be seamlessly added and combined. This differs from existing approaches such as SMT where the cooperation scheme is usually fixed (e.g., Nelson-Oppen). We contribute to two new cooperation schemes: (i) interval propagators completion that allows abstract domains to exchange bound constraints, and (ii) delayed product which exchanges over-approximations of constraints between two abstract domains. Moreover, the delayed product is based on delayed goal of logic programming, and it shows that abstract domains can also capture control aspects of constraint solving. Finally, to achieve modularity, we propose the shared product to combine abstract domains and cooperation schemes. Our approach has been fully implemented, and we provide various examples on the flexible job shop scheduling problem.

Keywords

abstract domainssolver cooperationmodularityconstraint programming
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 20 , Issue 6: 36th International Conference on Logic Programming Special Issue II , November 2020 , pp. 848 - 863
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Apt, K. R. 1999. The essence of constraint propagation. Theoretical computer science 221, 1-2, 179–210. https://doi.org/10.1016/S0304-3975(99)00032-8.Google Scholar
Benhamou, F., Goualard, F., Granvilliers, L., and Puget, J.-F. 1999. Revising hull and box consistency. In Proceedings of the 1999 International Conference on Logic Programming. 230–244. https://doi.org/10.7551/mitpress/4304.003.0024.Google Scholar
Brand, S., Narodytska, N., Quimper, C.-G., Stuckey, P., and Walsh, T. 2007. Encodings of the sequence constraint. In CP ’07. Springer, 210–224. https://doi.org/10.1007/978-3-540-74970-7_17.Google Scholar
Brucker, P. and Schlie, R. 1990. Job-shop scheduling with multi-purpose machines. Computing 45, 4 (Dec.), 369–375. https://doi.org/10.1007/BF02238804.Google Scholar
Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL ’77. ACM, 238–252. https://doi.org/10.1145/512950.512973.Google Scholar
Cousot, P., Cousot, R., and Mauborgne, L. 2012. Theories, solvers and static analysis by abstract interpretation. Journal of the ACM (JACM) 59, 6, 31. https://doi.org/10.1145/2395116.2395120.Google Scholar
D’Silva, V., Haller, L., and Kroening, D. 2014. Abstract satisfaction. In POPL ’14. ACM Press, 139–150. https://doi.org/10.1145/2535838.2535868.Google Scholar
Estévez-Martn, S., Hortalá-gonzález, T., Rodrguez-Artalejo, M., del Vado-Vírseda, R., Sáenz-Pérez, F., and Fernández, A. J. 2009. On the cooperation of the constraint domains H, R, and F in CFLP. Theory and Practice of Logic Programming 9, 4, 415–527. https://doi.org/10.1017/S1471068409003780.CrossRefGoogle Scholar
Fernández, A. J. and Hill, P. M. 2004. An interval constraint system for lattice domains. ACM Trans. Program. Lang. Syst. 26, 1 (Jan.), 1–46. https://doi.org/10.1145/963778.963779.Google Scholar
Hurink, J., Jurisch, B., and Thole, M. 1994. Tabu search for the job-shop scheduling problem with multi-purpose machines. Operations-Research-Spektrum 15, 4, 205–215. https://doi.org/10.1007/BF01719451.Google Scholar
Miné, A. 2006. The octagon abstract domain. Higher-Order and Symbolic Computation (HOSC) 19, 1, 31–100. https://doi.org/10.1007/s10990-006-8609-1.Google Scholar
Monfroy, E. 1998. An environment for designing/executing constraint solver collaborations. Electronic Notes in Theoretical Computer Science 16, 1, 1–22. https://doi.org/10.1016/S1571-0661(05)80588-2.Google Scholar
Nelson, G. and Oppen, D. C. 1979. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1, 2, 245–257. https://doi.org/10.1145/357073.357079.Google Scholar
Ohrimenko, O., Stuckey, P. J., and Codish, M. 2009. Propagation via lazy clause generation. Constraints 14, 3 (Sept.), 357–391. http://dx.doi.org/10.1007/s10601-008-9064-x.CrossRefGoogle Scholar
Older, W. 1993. Programming in CLP(BNR). In Position Papers for the First Workshop on Principles and Practice of Constraint Programming. 239–249.Google Scholar
Pelleau, M., Miné, A., Truchet, C., and Benhamou, F. 2013. A constraint solver based on abstract domains. In Verification, Model Checking, and Abstract Interpretation. Springer, 434–454. https://doi.org/10.1007/978-3-642-35873-9_26.Google Scholar
Schulte, C., Tack, G., and Lagerkvist, M. 2019. Modeling and Programming with Gecode.Google Scholar
Schutt, A., Feydy, T., and Stuckey, P. 2013. Scheduling optional tasks with explanation. In CP’13. 628–644. https://doi.org/10.1007/978-3-642-40627-0_47.Google Scholar
Talbot, P. 2019. Spacetime Programming: A Synchronous Language for Composable Search Strategies. In PPDP ’19. 18:1–18:16. https://doi.org/10.1145/3354166.3354183.Google Scholar
Talbot, P., Cachera, D., Monfroy, E., and Truchet, C. 2019. Combining Constraint Languages via Abstract Interpretation. In ICTAI ’19. 50–58. https://doi.org/10.1109/ICTAI.2019.00016.Google Scholar
Talbot, P., Éric, Monfroy, and Truchet, C. 2020. Modular constraint solver cooperation via abstract interpretation. http://arxiv.org/abs/2008.01415.Google Scholar
Ziat, G., Maréchal, A., Marie, P., Miné, A., and Truchet, C. 2019. Combination of Boxes and Polyhedra Abstractions for Constraint Solving. In NSAD ’19.Google Scholar