CP-SAT: `sufficient_assumptions_for_infeasibility()` returns a literal that is not in the assumption list (presolve only)

[proshkin-aitkn]

What version of OR-Tools and what language are you using?
Version: main @ commit 79e340fd50e1cae499bd6c9035486cf06c8261a5 (built from source). Also reproduces on stable v9.15.6755 (PyPI) and v9.14.6206 (PyPI).
Language: Python

Which solver are you using (e.g. CP-SAT, Routing Solver, GLOP, BOP, Gurobi)
CP-SAT

What operating system (Linux, Windows, ...) and version?
Linux. Reproduced on Ubuntu 24.04 with the stable PyPI wheel, and inside python:3.13-bookworm Docker for the master build.

What did you do?

CpSolver.sufficient_assumptions_for_infeasibility() is documented to return "a subset of the model assumptions that are sufficient to ensure infeasibility" (an MUS). With the default cp_model_presolve=True, it returns a literal index that was never passed to CpModel.add_assumptions(...). Disabling presolve returns a correct subset.

Minimal repro — run this script:

"""Minimal reproducer for an OR-Tools CP-SAT bug:

CpSolver.sufficient_assumptions_for_infeasibility() is documented to return
a subset of the model assumptions. With the default cp_model_presolve=True,
the returned list contains a literal that is NOT in the assumption list.
Disabling presolve returns the correct subset.
"""
from ortools.sat.python import cp_model


def build_model():
    """Tiny model with:
      - assumption literal `y` (the only assumption)
      - a constraint `y == 0` that makes `y=1` infeasible
      - a circuit constraint whose only arc into an otherwise isolated node is
        a self-loop gated on NOT(v), which forces v = 0
      - v is NEVER added to the assumption list
    The correct MUS is [y]; the bug returns [v] when presolve is enabled.
    """
    m = cp_model.CpModel()

    # v — forced to 0 by the circuit, never assumed.
    v = m.new_bool_var("v")
    # y — the assumption; `y == 0` makes `y=1` infeasible.
    y = m.new_bool_var("y")
    m.add(y == 0)

    # Two further bools used as circuit-node self-loop literals.
    a = m.new_bool_var("a")
    b = m.new_bool_var("b")

    # Tour over {0, 1, 2} plus an isolated node 99 whose only arc is a
    # self-loop gated on NOT(v). The circuit must pick that self-loop, so
    # v is forced to 0.
    arcs = [
        (0, 1, m.new_bool_var("arc_0_1")),
        (1, 0, m.new_bool_var("arc_1_0")),
        (0, 2, m.new_bool_var("arc_0_2")),
        (2, 0, m.new_bool_var("arc_2_0")),
        (1, 1, a.Not()),           # node 1 self-loop (optional)
        (2, 2, b.Not()),           # node 2 self-loop (optional)
        (99, 99, v.Not()),          # forces v = 0
    ]
    m.add_circuit(arcs)
    return m, v, y


def solve(model, presolve):
    s = cp_model.CpSolver()
    s.parameters.cp_model_presolve = presolve
    s.parameters.num_workers = 1
    status = s.solve(model)
    return s.status_name(status), list(s.sufficient_assumptions_for_infeasibility())


model, v, y = build_model()
model.add_assumptions([y])
assumptions = [y.index]

print(f"v.index = {v.index}  (NOT in assumptions)")
print(f"y.index = {y.index}  (the only assumption)")
print(f"assumptions = {assumptions}")
print()
for presolve in (True, False):
    m, v2, y2 = build_model()
    m.add_assumptions([y2])
    status, core = solve(m, presolve=presolve)
    bad = [c for c in core if c != y2.index]
    tag = "BUG" if bad else "OK"
    print(f"presolve={presolve!s:5}  status={status}  core={core}  "
          f"literals_not_in_assumptions={bad}  [{tag}]")

What did you expect to see

Both runs should return [y.index] (= [1]). The documented contract is that the returned list is a subset of the literals passed to add_assumptions(...).

What did you see instead?

v.index = 0  (NOT in assumptions)
y.index = 1  (the only assumption)
assumptions = [1]

presolve=True   status=INFEASIBLE  core=[0]  literals_not_in_assumptions=[0]  [BUG]
presolve=False  status=INFEASIBLE  core=[1]  literals_not_in_assumptions=[]  [OK]

With presolve enabled, the core is [0] — that is v's literal index, which was never added via add_assumptions. With presolve disabled, the core is [1] = y.index, the correct result.

[lperron]

It return the indices of the literals in the list

[proshkin-aitkn]

m = cp_model.CpModel()
y = m.new_bool_var("y")       # y.index == 0
m.add(y == 0)                  # y=1 is infeasible
d1 = m.new_bool_var("d1")     # d1.index == 1
d2 = m.new_bool_var("d2")     # d2.index == 2

# y is at POSITION 2 in the assumption list, but y.index == 0.
m.add_assumptions([d1, d2, y])

s = cp_model.CpSolver()
s.solve(m)
print(s.sufficient_assumptions_for_infeasibility())
# Output: [0]  -- this is y.index (variable index), NOT 2 (y's position in the list).

Produces [0] = y.index, not [2] = y's position. So the API returns variable indices, not list positions.

[fdid-git]

Yes, presolve and assumptions are currently a best effort support, we will need to improve that, but it might not happen soon. I will keep you posted.

If you want to keep presolve, you should at least turn on "keep_all_feasible_solutions_in_presolve:true" so we don't do simplification that might invalidate your assumptions. But even with that, you might run into the same issue you encountered, where we don't remap the internal variable correctly back.

[proshkin-aitkn]

I tried keep_all_feasible_solutions_in_presolve in my example and got the same result:

┌──────────┬───────────────────┬───────────────┬───────────┐
│ presolve │ keep_all_feasible │     core      │ correct?  │
├──────────┼───────────────────┼───────────────┼───────────┤
│ True     │ False             │ [0] (v.index) │ BUG       │
├──────────┼───────────────────┼───────────────┼───────────┤
│ False    │ False             │ [1] (y.index) │ OK        │
├──────────┼───────────────────┼───────────────┼───────────┤
│ True     │ True              │ [0] (v.index) │ still BUG │
├──────────┼───────────────────┼───────────────┼───────────┤
│ False    │ True              │ [1] (y.index) │ OK        │
└──────────┴───────────────────┴───────────────┴───────────┘