Solution hint and Assumptions reports wrong status when solved after presolve

[IgnaceBleukx]

Hi,

I am trying to use OR-tools with a combination of both assumptions and solution hinting. However, I've ran into the following problem where adding a solution hint to the model yields an invalid solution.

Below is a minimal example:

from ortools.sat.python import cp_model as ort

model = ort.CpModel()
solver = ort.CpSolver()

x = model.NewBoolVar("x")
y = model.NewBoolVar("y")

model.AddBoolOr([x])
model.AddBoolOr([~x, ~y])

model.AddHint(y,1)
model.AddAssumptions([y])

# solver.parameters.cp_model_presolve=False # uncommenting yields UNSAT
status = solver.Solve(model)

if status == ort.INFEASIBLE:
    print("Model is UNSAT")
else:
    print("Found solution")
>> Output: Found solution

Clearly, the model does not have a solution when we add the assumption y = 1. This is correctly found by the solver when turning off the solution hint, or by disabling presolve. However, when adding the solution hint and enabling presolve, the solver finds the following solution, which is invalid given the assumptions: [x = 1, y = 0]

I am using OR-Tools v9.10.4067 on Linux.

Kind regards, Ignace

[lperron]

you should print the actual status. I do not think it is OPTIMAL.

[IgnaceBleukx]

Hi, Thanks for the quick answer - the status is in fact optimal (code 4) when I print it after solving.

Attached is also the .proto of the model:

variables {
  name: "x"
  domain: 0
  domain: 1
}
variables {
  name: "y"
  domain: 0
  domain: 1
}
constraints {
  bool_or {
    literals: 0
  }
}
constraints {
  bool_or {
    literals: -1
    literals: -2
  }
}
solution_hint {
  vars: 1
  values: 1
}
assumptions: 1

[lperron]

OK. It is closed by presolve and we report a wrong status.

We will fix it, but low priority.