Search code examples
pythonsolveror-toolscp-sat

How to get detailed error messages for invalid OR-Tools CP-SAT models?


I'm trying to recreate the Google OR-Tools Stigler Diet example using the CP-SAT solver instead of the linear solver, and it results in a status of MODEL_INVALID. I don't know how to get detailed error messages or get any additional details as to why the model is invalid.

Looking into the Python source code, a code comment next to the definition of MODEL_INVALID says "The given CpModelProto didn't pass the validation step. You can get a detailed error by calling ValidateCpModel(model_proto)." But, I can't figure out how to access ValidateCpModel() and it's not referenced in the docs or any examples in the or-tools repo.

For reference, here's the program I'm trying to run:

from ortools.sat.python import cp_model
import sys


# Minimum and maximum values for each nutrient
nutritional_requirements = [  
    [1, 2],  # Vitamin A
    [1, 2],  # Vitamin B
    [1, 2],  # Vitamin C
]

# Nutritional value for each food
foods = [
  # Vitamins
  #  A  B  C
    [1, 0, 0],  # Food A
    [0, 1, 0],  # Food B
    [0, 0, 1],  # Food C
]

model = cp_model.CpModel()

quantity_of_food = [model.NewIntVar(0, sys.maxsize, str(i)) for i in range(len(foods))]

for i, nutrient in enumerate(nutritional_requirements):
    model.Add(
        sum([food[i] * quantity_of_food[i] for food in foods]) >= nutrient[0]
    )
    model.Add(
        sum([food[i] * quantity_of_food[i] for food in foods]) < nutrient[1]
    )

model.Minimize(sum(quantity_of_food))

solver = cp_model.CpSolver()
status = solver.Solve(model)

outcomes = [
    "UNKNOWN",
    "MODEL_INVALID",
    "FEASIBLE",
    "INFEASIBLE",
    "OPTIMAL",
]

print(outcomes[status])  # Prints "MODEL_INVALID"

This program seems pretty simple to me. How do I find a detailed error message explaining why the model is invalid?


Solution

  • There are two options:

    • solver.parameters.log_search_progress = True

    or

    • print(model.Validate())

    outputs

    Invalid model: var #0 domain do not fall in [kint64min + 2, kint64max - 1]. name: "0" domain: 0 domain: 9223372036854775807
    

    CP-SAT solvers rejects models that can overflow integer arithmetic. In particular, domains of variables should stay away from int64max.

    It is good practice to reduce the domain of variables as much as possible. It simplifies solving afterwards.