2026-07-24T11:53:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23874 2025-11-12T13:10:46Z ddc:004 open_access

Disjunctive Scheduling in Tempo Hebrard, Emmanuel Scheduling Constraint solvers Clause-learning In this paper we introduce a constraint programming lazy clause and literal generation solver embarking ideas from SAT Modulo theories. A key aspect of the solver are Boolean variables with an associated semantic in difference logic, i.e., systems of binary numeric difference constraints or edges, making it particularly adapted to scheduling and other temporal problems. We apply this solver to disjunctive scheduling problems, where edges are used as branching variables, can be inferred via the edge finding rule as well as by transitivity reasoning, and can in turn strengthen propagation via temporal graph reasoning. Our experiments on job-shop scheduling show that a deep integration of these techniques makes our solver competitive with state-of-the-art approaches on these problems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Emmanuel Hebrard 2025 Is Part Of LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2025.13 urn:nbn:de:0030-drops-238746 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.13 eng https://creativecommons.org/licenses/by/4.0/legalcode