Infeasibility and inconsistency¶

When submitting a model to LocalSolver (calling method solve), the expected result is to obtain a feasible solution, and even sometimes an optimal solution. However in some cases the returned solution can be infeasible in the sense that the current assignement of values to variables violates some of the constraints of the problem. Two solution statuses (see getSolutionStatus) are defined for these infeasibilty cases:

infeasible means that no feasible solution was found to the submitted problem but it could not be proven that no such solution exists. Maybe running a longer search would have produced a feasible solution.
inconsistent means that the solver was able to prove that no feasible solution exists. In this case, LocalSolver offers a functionality for analyzing the causes of this inconsistency.

Note

Note that both statuses infeasible and inconsistent can also be encountered on problems where no constraint was defined. Indeed, a solution where an objective takes an invalid value is considered infeasible. For instance minimize sqrt(x) implicitly requires that x takes a non-negative value.

Analyzing inconsistencies¶

Analyzing an inconsistent model amounts to identifying a relatively small inconsistent subproblem. Such a subproblem or inconsistency core is said to be irreductible if it contains no smaller inconsistent subproblem.

The function computeInconsistency computes such a core that is to say a set of expressions (named causes) such that the problem restricted to these expressions and their descendents is inconsistent. Calling this function requires the model to be closed and the solver to be stopped. This inconsistency core is returned as an LSInconsistency object. This object can be printed in a readable form so that the user can easily spot the origin of the inconsistency. It also allows scanning the set of identified causes.

For example, the following model is inconsistent because limiting the cube of y to 250 prevents y from taking values larger than 6, what make the constraint 3*x + y >= 20 impossible to satisfy:

function model() {
    x <- bool();
    y <- int(0,100);
    z <- bool();
    t <- int(0,100);
    constraint 3*x + y >= 20;
    constraint pow(y,3) <= 250;
    constraint 4*z + t <= 18;
    maximize x*t + 8*z*y;
}

The computation of the inconsistency core can be launched in the output function as follows:

function output() {
    iis = computeInconsistency();
    println(iis);
}

The resulting output on the standard console is the following:

...
Run output...
Computing inconsistency core...
Inconsistency core found with 2 causes.
Irreductible inconsistency core found with 2 causes.
2 causes in inconsistency core:
        pow(int(0, 100)#1, 3)  <=  250
        3  *  bool()#0  +  int(0, 100)#1  >=  20

The two constraints responsible for the inconsistency are identified and displayed. Note that expressions are identified by their type and index. It is also possible to assign names to variables in the model function:

x.name = "x";
y.name = "y";
z.name = "z";
t.name = "t";

Having defined these names the inconsistency core reads as follows:

2 causes in inconsistency core:
        pow(y, 3)  <=  250
        3  *  x  +  y  >=  20

In the APIs, the principle is the same.

Python
C++
C#
Java

Computing the inconsistency core is done through the compute_inconsistency method of the solver, which returns an LSInconsistency object.

This object can be converted to a string for display purpose. It is iterable, and contains the expressions in the inconsistency core.

# With ls a LocalSolver object
iis = ls.compute_inconsistency();
print(iis);

# With process a user-defined function
for expr in iis:
    process(expr)

Computing the inconsistency core is done through the computeInconsistency method of the solver, which returns an LSInconsistency object.

This object can be converted to a string for display purpose with toString. Individual expressions in the inconsistency core are accessed with getCause.

// With ls a LocalSolver object
iis = ls.computeInconsistency();
cout << iis.toString() << endl;

// With process a user-defined function
for (int i = 0; i < iis.getNbCauses(); ++i) {
    LSExpression expr = iis.getCause(i);
    process(expr)
}

Computing the inconsistency core is done through the ComputeInconsistency method of the solver, which returns an LSInconsistency object.

This object can be converted to a string for display purpose. Individual expressions in the inconsistency core are accessed with GetCause.

// With ls a LocalSolver object
iis = ls.ComputeInconsistency();
Console.WriteLine(iis);

// With Process a user-defined function
for (int i = 0; i < iis.GetNbCauses(); ++i) {
    LSExpression expr = iis.GetCause(i);
    Process(expr)
}

Computing the inconsistency core is done through the computeInconsistency method of the solver, which returns an LSInconsistency object.

This object can be converted to a string for display purpose. Inidividual expressions in the inconsistency core are accessed with getCause.

// With ls a LocalSolver object
iis = ls.computeInconsistency();
System.out.println(iis);

// With process a user-defined function
for (int i = 0; i < iis.getNbCauses(); ++i) {
    LSExpression expr = iis.getCause(i);
    process(expr)
}