CP-SAT returns UNKNOWN for production scheduling model despite presolve and feasible sub-models – looking for modeling advice

[gkmark3]

Hi everyone,

I'm working on a fairly large production scheduling application using Google OR-Tools CP-SAT in C# (.NET 8),
and I'd appreciate some advice on improving the model.

Application

The application runs on Azure Container Apps (ACA) having 16vCPU and generates production schedules, with 10min of execution time

The scheduler plans approximately 24–48 hours ahead using configurable time slots (typically 30 minutes).

Current model

Decision variables mainly represent

• Production quantity per (slot, mix)
• Delivery quantity
• storage inventory
• QC state
• Various helper variables for changeover logic

The model contains roughly

Presolved model

#Variables: 17,657

• 12,302 primary variables
• 7,515 Boolean variables

Constraints

• BoolOr: 6,935
• BoolAnd: 3,794
• ExactlyOne: 1,761
• AtMostOne: 1,354
• LinearN: 4,552

Symmetry graph

• 76,182 nodes
• 154,725 arcs

Solver Parameters:
max_time_in_seconds:600
num_search_workers:16
random_seed:1234
randomize_search:true
interleave_search:true
search_branching:PORTFOLIO_SEARCH
cp_model_presolve:true
linearization_level:1
symmetry_level:2
presolve_bve_threshold:500
log_search_progress:true
relative_gap_limit:0.01

Solver behavior

For some demand sets the solver finds an optimal solution quickly.

However, for certain combinations of demands, the solver returns

UNKNOWN

instead of FEASIBLE or OPTIMAL.

The same datasets become feasible if certain constraint groups are removed.

This suggests the model is not fundamentally infeasible.

---

Things already verified

I've already spent significant time isolating constraint groups.

Some observations:

• Individual constraint groups solve correctly.
• Most combinations solve correctly.
• UNKNOWN only appears when all business rules are enabled.
• Presolve succeeds.
• No obvious infeasible core remains.
• Objectives are currently disabled during debugging, and UNKNOWN still occurs.
• changed slot time from 30min to 1hr worked the schedule with all constraints (but this cannot be
  done now due to business complexity)

---

Current suspicion

I suspect this is no longer an infeasibility problem but rather a search/modeling issue.

The current model is quite SAT-heavy.

The changeover constraint currently introduces many helper BoolVars using

• OnlyEnforceIf
• BoolAnd
• BoolOr
• implications

to determine inter-slot changeovers.

After reviewing the model, I'm considering redesigning the changeover logic to
reduce the number of Boolean helper variables significantly.

---

Questions

1. Looking only at the presolved statistics, do these numbers suggest a SAT-heavy model likely to produce UNKNOWN?

2. Are there particular constraint patterns that typically cause CP-SAT to stall in scheduling models?

3. Is there a recommended way to model changeovers between production slots without introducing large implication networks?

4. Would you generally prefer:

   • more integer state variables with fewer BoolVars
   • or the opposite?

5. Are there any common modeling anti-patterns that stand out from the statistics above?

6. Would enabling LNS or changing search parameters likely help here, or is this more likely a modeling issue?

---

Any suggestions on improving the model formulation would be greatly appreciated.

Thanks!

[jmarca]

Did you try increasing the time to see how much time it needs to find a solution? If you let it run for 20 or 30 minutes instead of 10, does it work?

…

On Thu, Jul 16, 2026 at 04:07:09AM -0700, gkmark3 wrote: Hi everyone, I'm working on a fairly large production scheduling application using Google OR-Tools CP-SAT in C# (.NET 8), and I'd appreciate some advice on improving the model. ## Application The application runs on Azure Container Apps (ACA) having 16vCPU and generates production schedules, with 10min of execution time The scheduler plans approximately 24–48 hours ahead using configurable time slots (typically 30 minutes). --- ## Current model Decision variables mainly represent - Production quantity per (slot, mix) - Delivery quantity - storage inventory - QC state - Various helper variables for changeover logic The model contains roughly Presolved model #Variables: 17,657 - 12,302 primary variables - 7,515 Boolean variables Constraints - BoolOr: 6,935 - BoolAnd: 3,794 - ExactlyOne: 1,761 - AtMostOne: 1,354 - LinearN: 4,552 Symmetry graph - 76,182 nodes - 154,725 arcs Solver Parameters: max_time_in_seconds:600 num_search_workers:16 random_seed:1234 randomize_search:true interleave_search:true search_branching:PORTFOLIO_SEARCH cp_model_presolve:true linearization_level:1 symmetry_level:2 presolve_bve_threshold:500 log_search_progress:true relative_gap_limit:0.01 --- ## Solver behavior For some demand sets the solver finds an optimal solution quickly. However, for certain combinations of demands, the solver returns UNKNOWN instead of FEASIBLE or OPTIMAL. The same datasets become feasible if certain constraint groups are removed. This suggests the model is not fundamentally infeasible. --- ## Things already verified I've already spent significant time isolating constraint groups. Some observations: - Individual constraint groups solve correctly. - Most combinations solve correctly. - UNKNOWN only appears when all business rules are enabled. - Presolve succeeds. - No obvious infeasible core remains. - Objectives are currently disabled during debugging, and UNKNOWN still occurs. - changed slot time from 30min to 1hr worked the schedule with all constraints (but this cannot be done now due to business complexity) --- ## Current suspicion I suspect this is no longer an infeasibility problem but rather a search/modeling issue. The current model is quite SAT-heavy. The changeover constraint currently introduces many helper BoolVars using - OnlyEnforceIf - BoolAnd - BoolOr - implications to determine inter-slot changeovers. After reviewing the model, I'm considering redesigning the changeover logic to reduce the number of Boolean helper variables significantly. --- ## Questions 1. Looking only at the presolved statistics, do these numbers suggest a SAT-heavy model likely to produce UNKNOWN? 2. Are there particular constraint patterns that typically cause CP-SAT to stall in scheduling models? 3. Is there a recommended way to model changeovers between production slots without introducing large implication networks? 4. Would you generally prefer: - more integer state variables with fewer BoolVars - or the opposite? 5. Are there any common modeling anti-patterns that stand out from the statistics above? 6. Would enabling LNS or changing search parameters likely help here, or is this more likely a modeling issue? --- Any suggestions on improving the model formulation would be greatly appreciated. Thanks! -- Reply to this email directly or view it on GitHub: #5259 You are receiving this because you are subscribed to this thread. Message ID: ***@***.***>

-- James E. Marca Activimetrics LLC

[gkmark3]

Tried almost 45min, still got UNKNOWN