Modular constraint solver cooperation via abstract interpretation

DOI10.1017/S1471068420000162MaRDI QIDQ5140021zbMATH OpenFDO

Authors Pierre Talbot, Eric Monfroy, Charlotte Truchet

Publication date 13 December 2020

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2008.01415

zbMATH Keywords

abstract domainsconstraint programmingmodularitysolver cooperation

Mathematics Subject Classification ID

Logic programming (68N17) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Deterministic scheduling theory in operations research (90B35)

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. Under consideration for acceptance in TPLP.

Recommendations

• scientific article; zbMATH DE number 2080334
• scientific article; zbMATH DE number 1822298
• scientific article; zbMATH DE number 1696806
• A proposal for the cooperation of solvers in constraint functional logic programming
• A constraint solver based on abstract domains

Cites work

• A constraint solver based on abstract domains
• Abstract satisfaction
• Encodings of the Sequence Constraint
• Job-shop scheduling with multi-purpose machines
• On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP
• Propagation via lazy clause generation
• Simplification by Cooperating Decision Procedures
• Tabu search for the job-shop scheduling problem with multi-purpose machines
• The essence of constraint propagation
• The octagon abstract domain
• Theories, solvers and static analysis by abstract interpretation

Cited in

(4)

• Constraint-based analysis of composite solvers
• scientific article; zbMATH DE number 1231676 (Why is no real title available?)
• scientific article; zbMATH DE number 2080334 (Why is no real title available?)
• scientific article; zbMATH DE number 1822298 (Why is no real title available?)

Describes a project that uses

Uses Software

• Gecode

This page was built for publication: Modular constraint solver cooperation via abstract interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5140021)