-
Notifications
You must be signed in to change notification settings - Fork 2.4k
Description
What language and solver does this apply to?
CP-SAT, v9.15
Describe the problem you are trying to solve.
I have encountered a performance regression in specific scheduling models where the solver becomes stuck for hours, whereas disabling the presolver allows these same models to solve in seconds.
Upon investigation, it appears that the presolver converts NoOverlap constraints into AllDiff constraints when all intervals are unit-sized. While this is a logical simplification, it seems to strip away the scheduling specific machinery that makes CP-SAT efficient for these problems. This likely includes scheduling-specific cuts, LNS (even though I did not have LNS workers in my portfolio in the feasibility instances I was working with), scheduling based decision strategies, and no overlap propagation that incorporates precedences. In these instances, the benefit of the AllDiff simplification seems to be significantly outweighed by the loss of the scheduling context.
Describe the solution you'd like
I would like a way to opt-out of this specific transformation through SatParameters. This could be achieved by adding a new parameter specifically for this conversion or perhaps by extending the existing infer_all_diffs parameter to cover this case as well.
Describe alternatives you've considered
I have verified this behavior with a workaround: by adding a single interval of size greater than one to the constraint (for instance, placed beyond the makespan), I can prevent the presolver from identifying the constraint as "all unit." This preserves the scheduling machinery and returns the solve time to seconds.
Additional context
If this is difficult to reproduce internally, I can look into extracting and cleaning a model protobuf to demonstrate the performance impact. It would take some effort on my end to isolate a shareable version, so please let me know if it’s essential for your investigation.