CP-SAT: Best way to find infeasible constraints

[Phibedy]

Is there some builtin method to get the constraints which can't be solved?

If not would it be better to try

• to solve it ignoring one element after the other (permutations or maybe some smart search)
• make all constraints optionally by introducing a boolean variable which states if the constraint should hold. Afterwards the sum of all booleans is maximized

Thank you for your time 👍

[lperron]

which solver? Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00 Le mar. 11 déc. 2018 à 15:11, Phibedy <notifications@github.com> a écrit :

…

Is there some builtin method to get the constraints which can't be solved? If not would it be better to try - to solve it ignoring one element after the other (permutations or maybe some smart search) - make all constraints optionally by introducing a boolean variable which states if the constraint should hold. Afterwards the sum of all booleans is maximized Thank you for your time 👍 — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#973>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AKj17dAIOWSKhXemyk1nG--znSIfKG6Xks5u370LgaJpZM4ZNfMK> .

[Phibedy]

Sorry missed that, cp-sat

[lperron]

A sad answer as the SAT solver knows more, but the code is not yet written.

1. Yes, you can do better than 1 constraint at a time. See QuickXPlain https://pdfs.semanticscholar.org/dee6/53e324b42311f93adf83611a985028f8b54c.pdf
2. Not all constraints supports enforcement literals, mostly boolean constraints (except xor), and linear one + interval variables. So option 2 may not be feasible.

If feasible, I would use option 2, but not all constraints accept enforcement literals.

[eblume]

Regarding option 2, specifically XOr,

can't you just enforce XOr like such?

model.Add(sum(boolean_constraints) == 1).OnlyEnforceIf(enforcement_literal)

I was curious as to why XOr wasn't allowed to have an enforcement literal, and have used the above successfully.

---

Regarding the topic of finding infeasible constraints: is there any update on adding this feature to CP-SAT, and can I help? This would be a very large help to me, as currently I am working around it by re-running the problem with manual relaxations, and it's getting complicated very fast.

Thank you very much!

[lperron]

xor works on an array. For 2 booleans, this is easy. For n booleans, the definition of sum is odd, which has a specialized propagator, that does not yet support enforcement literals. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00 Le sam. 20 avr. 2019 à 22:32, Erich Blume <notifications@github.com> a écrit :

…

Regarding option 2, specifically XOr, can't you just enforce XOr like such? model.Add(sum(boolean_constraints) == 1).OnlyEnforceIf(enforcement_literal) I was curious as to why XOr wasn't allowed to have an enforcement literal, and have used the above successfully. ------------------------------ Regarding the topic of finding infeasible constraints: is there any update on adding this feature to CP-SAT, and can I help? This would be a very large help to me, as currently I am working around it by re-running the problem with manual relaxations, and it's getting complicated very fast. Thank you very much! — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#973 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACUPL3MNMPW7DJCH6NUIGVDPRN4U7ANCNFSM4GJV6MFA> .

[eblume]

Thank you for the real-time response! I wasn't aware that xor on an array was considered sum-mod-2 in boolean algebra. For the concept of "One and only one of these LinearExpressions MUST be true", is my formulation (sum(...) == 1) sufficient? It appears to work, although perhaps that is what is causing my unexpected 'INFEASIBLE' problem.

[lperron]

It is valid only if n = 2 Otherwise, create an extra integer variable, and add sum(n) - 2 * extra_var == 1. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00 Le sam. 20 avr. 2019 à 22:39, Erich Blume <notifications@github.com> a écrit :

…

Thank you for the real-time response! I wasn't aware that xor on an array was considered sum-mod-2 in boolean algebra. For the concept of "One and only one of these LinearExpressions MUST be true", is my formulation (sum(...) == 1) sufficient? It appears to work, although perhaps that is what is causing my unexpected 'INFEASIBLE' problem. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#973 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACUPL3POTMEO74AE76Z4JFTPRN5QJANCNFSM4GJV6MFA> .

[joegaudet]

Hey Guys,

Also wondering if there is anyway to determine which constraint is causing infeasibility, simply to report it back to the user.

[lalithsuresh]

@joegaudet not yet: #1565

Not sure if it's on their roadmap.

[lperron]

Not yet. We have too much to do in the performance of the solver before that. Le mar. 10 sept. 2019 à 18:06, Lalith Suresh <notifications@github.com> a écrit :

…

@joegaudet <https://github.com/joegaudet> not yet: #1565 <#1565> Not sure if it's on their roadmap. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#973?email_source=notifications&email_token=ACUPL3JLYKKBNUFF5VHBCQLQI7AZXA5CNFSM4GJV6MFKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD6LUNQA#issuecomment-530007744>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACUPL3MCOB46TCZGXODELXTQI7AZXANCNFSM4GJV6MFA> .

[trianta2]

I too would find this feature very useful

[ykzeng]

I second @trianta2 , many times the constraints are built on the fly based on real-world parameters which may not be feasible, so it would be nice to be able to identify those constraints that is preventing the optimization