[CP-SAT] Need support to understand infeability criteria

[maximouton]

Hello,

I am working on a planing generation project which includes rather complex contraints. I implemented two versions of the same engine using CBC and CP-SAT with similar capabilities. The CBC version works well so is working the CP-SAT version except for one type of constraint that make the problem infeasible. This constraint is a "people affinity" contraint which provide objectives of occurrence where people work together.

In general when I read solver logs I can identify the constraint that makes the solver unable to solve but in this case I see no relevant information.

I there any way to get more detail on the reason why the solver state that the model is infeasible during pre-solving? Can I influence the infeasibility criteria?

Here is the log I get when I enable the problematic constraint:

Starting CP-SAT solver v9.7.2996
Parameters: log_search_progress: true enumerate_all_solutions: true log_to_stdout: true
Setting number of workers to 1

Initial optimization model '': (model_fingerprint: 0xa7ffd9e5010759a6)
#Variables: 12'189 (#bools: 4'494 in objective)
  - 11'894 Booleans in [0,1]
  - 32 in [-2147483648,2147483647]
  - 32 in [0,6]
  - 214 in [0,21]
  - 17 in [0,32]
#kBoolAnd: 2'278 (#enforced: 2'278) (#literals: 8'296)
#kBoolOr: 2'278 (#enforced: 2'278) (#literals: 6'018)
#kLinear0: 64 (#enforced: 64)
#kLinear1: 13'135 (#enforced: 10'604)
#kLinear2: 1'147 (#enforced: 64)
#kLinearN: 5'413 (#enforced: 2'584) (#terms: 85'325)

Starting presolve at 0.04s
INFEASIBLE: ''

Presolve summary:
  - 0 affine relations were detected.
Problem closed by presolve.
CpSolverResponse summary:
status: INFEASIBLE
objective: NA
best_bound: NA
integers: 0
booleans: 0
conflicts: 0
branches: 0
propagations: 0
integer_propagations: 0
restarts: 0
lp_iterations: 0
walltime: 0.0772253
usertime: 0.0772256
deterministic_time: 0
gap_integral: 0

Another separate question I have is related to model I print using model.ExportToFile.

I am able to track constraint in the model file and there is something I found strange when i set a boolVar and its opposite for instance with this statement (I am using .NET):

model.AddBoolAnd(segmentsVars).OnlyEnforceIf(worksToday);
model.AddBoolOr(segmentsVarsI).OnlyEnforceIf(worksToday.Not());

The result I see in the model is the following:

constraints {
  enforcement_literal: [6986]
  bool_and {
    literals: [6984, 6985]
  }
}
constraints {
  enforcement_literal: [-6987]
  bool_or {
    literals: [-6985, -6986]
  }
}

I would have expected something like this for the second constraint:

constraints {
  enforcement_literal: [-6986]
  bool_or {
    literals: [-6984, -6985]
  }
}

Am I wrong?

Thanks for support

Maximilien

[Frederic Didier]

Can you send us the cp_model.protol? so we can try to improve the logging. thanks.

 

Another separate question I have is related to model I print using model.ExportToFile.

I am able to track constraint in the model file and there is something I found strange when i set a boolVar and its opposite for instance with this statement (I am using .NET):

model.AddBoolAnd(segmentsVars).OnlyEnforceIf(worksToday);
model.AddBoolOr(segmentsVarsI).OnlyEnforceIf(worksToday.Not());

The result I see in the model is the following:

constraints {
  enforcement_literal: [6986]
  bool_and {
    literals: [6984, 6985]
  }
}
constraints {
  enforcement_literal: [-6987]
  bool_or {
    literals: [-6985, -6986]
  }
}

This is normal, not(lit) = - lit - 1.

Otherwise not(0) == 0.

 

I would have expected something like this for the second constraint:

constraints {
  enforcement_literal: [-6986]
  bool_or {
    literals: [-6984, -6985]
  }
}

Am I wrong?

Thanks for support

Maximilien

--
You received this message because you are subscribed to the Google Groups "or-tools-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/9e9fb587-287c-47b2-a83e-16186fabddd2n%40googlegroups.com.

[maximouton]

Here is the file corresponding to the log from my previous message.

Thanks

[maximouton]

And a version with all other contraints removed except the one.

Still there the CP-SAT considers the model infeasible.

[Frederic Didier]

Thanks, I will update the code to display more information.

On the last problem, this is what I now have:

INFEASIBLE: 'proven during initial copy of constraint #54:
name: "54_AddRelaxedPersonBalanceConstraint_11_3_4_NaN_NaN_NaN_day_0" linear { vars: 4514 vars: 4517 coeffs: 1 coeffs: 1 domain: 4 domain: 9223372036854775807 }
  var:4514 domain:[0,1]
  var:4517 domain:[0,1]
'

Where you can see clearly that you can never have >= 4 with just two Booleans.

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/1b0180f1-79b9-402d-9ebd-2084dddbf914n%40googlegroups.com.

[maximouton]

Thank you very much, that will help a lot.. and thank for the hint on my problem I guess I will manage to solve my issue.