Or-tools: 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 :+1:

[lperron]

which solver?
Laurent Perron | Operations Research | [email protected] | (33) 1 42 68 53
00

Le mar. 11 déc. 2018 à 15:11, Phibedy [e-mail] 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
https://github.com/google/or-tools/issues/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 | [email protected] | (33) 1 42 68 53
00

Le sam. 20 avr. 2019 à 22:32, Erich Blume [e-mail] 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
https://github.com/google/or-tools/issues/973#issuecomment-485166089,
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 | [email protected] | (33) 1 42 68 53
00

Le sam. 20 avr. 2019 à 22:39, Erich Blume [e-mail] 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
https://github.com/google/or-tools/issues/973#issuecomment-485167353,
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: https://github.com/google/or-tools/issues/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 [e-mail] a
écrit :

@joegaudet https://github.com/joegaudet not yet: #1565
https://github.com/google/or-tools/issues/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
https://github.com/google/or-tools/issues/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

[joegaudet]

@Mizux curious if there's any timeline on this, I see that it's been added to the TODO file. This tool is great, however it's very challenging to identify the source of issues with infeasibility.

[javiermas]

Same here. It's really a pain to debug problems with the model. Particularly when you're using it with a myriad of input data. This has been our biggest problem by far with the ortools library.

[joegaudet]

We end up having to use heuristics to try and determine which input is
likely the issue.

On Thu, Sep 17, 2020 at 6:53 AM Javier Mas Adell [e-mail]
wrote:

Same here. It's really a pain to debug problems with the model.
Particularly when you're using it with a myriad of input data. This has
been our biggest problem by far with the ortools library.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-694250667,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/AAA6IB734I7ZRTEHYOLTADLSGIIE3ANCNFSM4GJV6MFA
.

[joegaudet]

@Mizux noticed you moved this in Feature Requests, curious if there's any sort of timeline on it? Quarters? Years?

Certainly appreciate all of the work people have done putting this together, just trying to plan what we might be able to do to address failing constraints on our system.

[lperron]

In the general sense, give a model, find why it is infeasible, probably
never. I do not believe this is the right approach.
I understand it is needed to find a stupidly wrong constraint (bad data),
but in the general case, the result is unusable.

What you can do is instrument your code with enforcement literals. This
part is a bit tricky only linear constraints, Boolean constraints, and
intervals support enforcement literals. But in the end, you want to achieve:

literal1 => one part of the model
literal2 => another part of the model.

Then you want a minimal number of false literal to get a feasible model.

You can do either by minimizing the (weighted) sum of literals, or adding
them as assumptions in the model.
Then the solver will try to heuristically find a (local) minimum assignment
of false literals to get a feasible model.

Both are already available, but I did not have the time to document it.

Laurent Perron | Operations Research | [email protected] | (33) 1 42 68 53
00

Le mar. 27 oct. 2020 à 23:35, Joe Gaudet [e-mail] a
écrit :

@Mizux https://github.com/Mizux noticed you moved this in Feature
Requests, curious if there's any sort of timeline on it? Quarters? Years?

Certainly appreciate all of the work people have done putting this
together, just trying to plan what we might be able to do to address
failing constraints on our system.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717580648,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/ACUPL3IAP7REHA3LKI4KIADSM5DLRANCNFSM4GJV6MFA
.

[joegaudet]

I'm not sure I follow, if I have a variety of inequalities in my model,
from the summing of assignment Booleans. How can I tell that one cannot be
satisfied in the presence of another inequality?

Is there an example of using enforcement literals in python?
On Tue, Oct 27, 2020 at 5:13 PM Laurent Perron [e-mail]
wrote:

In the general sense, give a model, find why it is infeasible, probably
never. I do not believe this is the right approach.
I understand it is needed to find a stupidly wrong constraint (bad data),
but in the general case, the result is unusable.

What you can do is instrument your code with enforcement literals. This
part is a bit tricky only linear constraints, Boolean constraints, and
intervals support enforcement literals. But in the end, you want to
achieve:

literal1 => one part of the model
literal2 => another part of the model.

Then you want a minimal number of false literal to get a feasible model.

You can do either by minimizing the (weighted) sum of literals, or adding
them as assumptions in the model.
Then the solver will try to heuristically find a (local) minimum assignment
of false literals to get a feasible model.

Both are already available, but I did not have the time to document it.

Laurent Perron | Operations Research | [email protected] | (33) 1 42 68
53
00

Le mar. 27 oct. 2020 à 23:35, Joe Gaudet [e-mail] a
écrit :

@Mizux https://github.com/Mizux noticed you moved this in Feature
Requests, curious if there's any sort of timeline on it? Quarters? Years?

Certainly appreciate all of the work people have done putting this
together, just trying to plan what we might be able to do to address
failing constraints on our system.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717580648,
or unsubscribe
<
https://github.com/notifications/unsubscribe-auth/ACUPL3IAP7REHA3LKI4KIADSM5DLRANCNFSM4GJV6MFA

.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717615603,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/AAA6IB3AOWW2EW43FJJOLGLSM5OZ3ANCNFSM4GJV6MFA
.

[lperron]

Each inequality has an enforcement literal.
Then you maximize the sum of enforcement literals.
Laurent Perron | Operations Research | [email protected] | (33) 1 42 68 53
00

Le mer. 28 oct. 2020 à 01:55, Joe Gaudet [e-mail] a
écrit :

I'm not sure I follow, if I have a variety of inequalities in my model,
from the summing of assignment Booleans. How can I tell that one cannot be
satisfied in the presence of another inequality?

Is there an example of using enforcement literals in python?
On Tue, Oct 27, 2020 at 5:13 PM Laurent Perron [e-mail]
wrote:

In the general sense, give a model, find why it is infeasible, probably
never. I do not believe this is the right approach.
I understand it is needed to find a stupidly wrong constraint (bad data),
but in the general case, the result is unusable.

What you can do is instrument your code with enforcement literals. This
part is a bit tricky only linear constraints, Boolean constraints, and
intervals support enforcement literals. But in the end, you want to
achieve:

literal1 => one part of the model
literal2 => another part of the model.

Then you want a minimal number of false literal to get a feasible model.

You can do either by minimizing the (weighted) sum of literals, or adding
them as assumptions in the model.
Then the solver will try to heuristically find a (local) minimum
assignment
of false literals to get a feasible model.

Both are already available, but I did not have the time to document it.

Laurent Perron | Operations Research | [email protected] | (33) 1 42 68
53
00

Le mar. 27 oct. 2020 à 23:35, Joe Gaudet [e-mail] a
écrit :

@Mizux https://github.com/Mizux noticed you moved this in Feature
Requests, curious if there's any sort of timeline on it? Quarters?
Years?

Certainly appreciate all of the work people have done putting this
together, just trying to plan what we might be able to do to address
failing constraints on our system.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<https://github.com/google/or-tools/issues/973#issuecomment-717580648
,
or unsubscribe
<

https://github.com/notifications/unsubscribe-auth/ACUPL3IAP7REHA3LKI4KIADSM5DLRANCNFSM4GJV6MFA
>

.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717615603,
or unsubscribe
<
https://github.com/notifications/unsubscribe-auth/AAA6IB3AOWW2EW43FJJOLGLSM5OZ3ANCNFSM4GJV6MFA

.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717628201,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/ACUPL3MGJAR5MKX4UFNMQO3SM5TXLANCNFSM4GJV6MFA
.

[joegaudet]

But if the constraints themselves are _requirements_ which is to say if
they cannot be solved the model cannot be solver. I'm not sure I understand
how maximizing them would help?

Could you give a pseudo-code example?

.joe

On Wed, Oct 28, 2020 at 12:05 AM Laurent Perron [e-mail]
wrote:

Each inequality has an enforcement literal.
Then you maximize the sum of enforcement literals.
Laurent Perron | Operations Research | [email protected] | (33) 1 42 68
53
00

Le mer. 28 oct. 2020 à 01:55, Joe Gaudet [e-mail] a
écrit :

I'm not sure I follow, if I have a variety of inequalities in my model,
from the summing of assignment Booleans. How can I tell that one cannot
be
satisfied in the presence of another inequality?

Is there an example of using enforcement literals in python?
On Tue, Oct 27, 2020 at 5:13 PM Laurent Perron <[email protected]

wrote:

In the general sense, give a model, find why it is infeasible, probably
never. I do not believe this is the right approach.
I understand it is needed to find a stupidly wrong constraint (bad
data),
but in the general case, the result is unusable.

What you can do is instrument your code with enforcement literals. This
part is a bit tricky only linear constraints, Boolean constraints, and
intervals support enforcement literals. But in the end, you want to
achieve:

literal1 => one part of the model
literal2 => another part of the model.

Then you want a minimal number of false literal to get a feasible
model.

You can do either by minimizing the (weighted) sum of literals, or
adding
them as assumptions in the model.
Then the solver will try to heuristically find a (local) minimum
assignment
of false literals to get a feasible model.

Both are already available, but I did not have the time to document it.

Laurent Perron | Operations Research | [email protected] | (33) 1 42
68
53
00

Le mar. 27 oct. 2020 à 23:35, Joe Gaudet [e-mail] a
écrit :

@Mizux https://github.com/Mizux noticed you moved this in Feature
Requests, curious if there's any sort of timeline on it? Quarters?
Years?

Certainly appreciate all of the work people have done putting this
together, just trying to plan what we might be able to do to address
failing constraints on our system.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<
https://github.com/google/or-tools/issues/973#issuecomment-717580648
,
or unsubscribe
<

https://github.com/notifications/unsubscribe-auth/ACUPL3IAP7REHA3LKI4KIADSM5DLRANCNFSM4GJV6MFA

>

.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<https://github.com/google/or-tools/issues/973#issuecomment-717615603
,
or unsubscribe
<

https://github.com/notifications/unsubscribe-auth/AAA6IB3AOWW2EW43FJJOLGLSM5OZ3ANCNFSM4GJV6MFA
>

.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717628201,
or unsubscribe
<
https://github.com/notifications/unsubscribe-auth/ACUPL3MGJAR5MKX4UFNMQO3SM5TXLANCNFSM4GJV6MFA

.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-717744251,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/AAA6IB2PHRB5XZN4GOZTMWDSM67D3ANCNFSM4GJV6MFA
.

[lalithsuresh]

@joegaudet what Laurent means is to re-run the model but with all the constraints having an enforcement literal attached (so you'll have to modify your code or have a way to conditionally attach these literals in your code). You then have to add a new objective function which maximizes the sum of these enforcement literals. Once a solution is found, the literals that are false point to the "infeasible constraints".

This should work as long as your constraints support enforcement literals, but not all do, which is the drawback (e.g., cumulative and other scheduling constraints).

[joegaudet]

Ahhhh gotcha. Is there an example of these literals in python somewhere? I currently re run a setup manually when some constraints are fungible.

[lperron]

Yes. But scheduling uses intervals that support enforcement literals. The
circuit constraint supports bon visited nodes

So this is tedious, but should be feasible.

Le mer. 28 oct. 2020 à 20:56, Lalith Suresh [e-mail] a
écrit :

@joegaudet https://github.com/joegaudet what Laurent means is to re-run
the model but with all the constraints having an enforcement literal
attached (so you'll have to modify your code or have a way to conditionally
attach these literals in your code). You then have to add a new objective
function which maximizes the sum of these enforcement literals. Once a
solution is found, the literals that are false point to the "infeasible
constraints".

This should work as long as your constraints support enforcement literals,
but not all do, which is the drawback (e.g., cumulative and other
scheduling constraints).

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-718173242,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/ACUPL3P5MKBCNOJIH5AOJ3TSNBZOXANCNFSM4GJV6MFA
.

[lalithsuresh]

@lperron One question though. You mentioned earlier in thread that the solver "knows more". My understanding was that the CP-SAT solver computes cores as part of the search process, but is the problem that these cores are hard to meaningfully relate back into vars/constraints in the input model?

[lperron]

The problem with explanation is that they are hard to process.
You will get a lot of constraints, including all the trivial consistency
constraints of the model.

To be useful, explanations need to be targeted. In practise, you decompose
the model into a background model and an active model.

To use the cores, you need to fill this field in the model proto:

// A list of literals. The model will be solved assuming all these
literals
// are true. Compared to just fixing the domain of these literals, using
this
// mechanism is slower but allows in case the model is INFEASIBLE to get a
// potentially small subset of them that can be used to explain the
// infeasibility.
//
// Think (IIS), except when you are only concerned by the provided
// assumptions. This is powerful as it allows to group a set of logically
// related constraint under only one enforcement literal which can
potentially
// give you a good and interpretable explanation for infeasibility.
//
// Such infeasibility explanation will be available in the
// sufficient_assumptions_for_infeasibility response field.
repeated int32 assumptions = 7;

This replaces the sum(literals) objective. It will be much faster, but the
resulting explanation will not be proven minimal, just a heuristic result.
Laurent Perron | Operations Research | [email protected] | (33) 1 42 68 53
00

Le mer. 28 oct. 2020 à 21:06, Lalith Suresh [e-mail] a
écrit :

@lperron https://github.com/lperron One question though. You mentioned
earlier in thread that the solver "knows more". My understanding was that
the CP-SAT solver computes cores as part of the search process, but is the
problem that these cores are hard to meaningfully relate back into
vars/constraints in the input model?

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/google/or-tools/issues/973#issuecomment-718178052,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/ACUPL3NZ5PZFFWWBAEW5U4LSNB2STANCNFSM4GJV6MFA
.

[lalithsuresh]

Thanks @lperron! This is quite the hidden gem. :) I just gave it a spin and think this would be quite useful already.

For everyone else, here's an example in Java.

    @Test
    public void assumptionsTest() {
        final CpModel model = new CpModel();
        final IntVar v1 = model.newBoolVar("v1");
        final IntVar v2 = model.newBoolVar("v2");
        final IntVar i1 = model.newIntVar(0, 5, "i1");
        final IntVar i2 = model.newIntVar(0, 5, "i2");

        model.addGreaterOrEqual(LinearExpr.sum(new IntVar[]{i1, i2}), 11).onlyEnforceIf(v1); // can't be satisfied
        model.addLessOrEqual(LinearExpr.sum(new IntVar[]{i1, i2}), 5).onlyEnforceIf(v2);
        model.getBuilder().addAssumptions(v1.getIndex());
        model.getBuilder().addAssumptions(v2.getIndex());

        final CpSolver solver = new CpSolver();
        final CpSolverStatus status = solver.solve(model);

        assertEquals(CpSolverStatus.INFEASIBLE, status);
        for (final int varIndex: solver.response().getSufficientAssumptionsForInfeasibilityList()) {
            System.out.println(model.getBuilder().getVariables(varIndex)); // correctly prints variable "v1"
        }
    }