New answers tagged


It looks like your first constraint should instead be $$0b_1 + a_1 b_2 + a_2 b_3 - d \le 0$$ With this change, the logical implications are \begin{align} b_1 = 1 &\implies 0 \le d \le a_1 \\ b_2 = 1 &\implies a_1 \le d \le a_2 \\ b_3 = 1 &\implies a_2 \le d \le a_3 \end{align} To avoid ambiguous borders, introduce a small tolerance $\epsilon>...


CP-SAT uses a SAT backend. But at any moment, just like with SMT solvers, the full model is never fully represented using clauses and Boolean literals. I recommend looking at the CPAIOR 2020 masterclass on CP (on YouTube) to get a better understanding of the architecture of the solver.

Top 50 recent answers are included