OR-tools gives UNSAT while SAT

[IgnaceBleukx]

Given in the zip file is a model for which OR-tools returns UNSAT.

However, there does exist a model, which I have filled in by fixing vars, then OR-tools does return SAT as it should be.

Either this is an issue in our _post_constraint but it looks like an OR-tools issue...
models.zip

[IgnaceBleukx]

Did some more digging, it looks like an OR-tools issue indeed. Will post on their github page.
I ran all constraints trough the transformations and created a new model with some more friendly names. Result below:

from ortools.sat.python import cp_model as ort

model = ort.CpModel()

a = model.NewIntVar(0,3,"a")
b = model.NewIntVar(0,3,"b")
c = model.NewIntVar(0,3,"c")
d = model.NewIntVar(0,3,"d")

p = model.NewIntVar(0,3,"p")
q = model.NewIntVar(0,3,"q")
r = model.NewIntVar(0,3,"r")
s = model.NewIntVar(0,3,"s")

bv1 = model.NewBoolVar("bv1")
bv2 = model.NewBoolVar("bv2")
bv3 = model.NewBoolVar("bv3")


model.Add(b != 1)
model.Add(b != 2)

model.Add(c != 0)
model.Add(c != 3)

model.Add(d != 0)

model.Add(p != 2)
model.Add(p != 3)

model.Add(q != 1)

model.Add(r != 1)

model.Add(s != 2)

model.AddAllDifferent([a,b,c,d])
model.AddAllDifferent([p,q,r,s])

model.Add(a == 0).OnlyEnforceIf(bv1)
model.Add(r == 0).OnlyEnforceIf(bv2)
model.AddBoolOr([bv2,bv3])
model.Add(a == 2).OnlyEnforceIf(bv3)
model.Add(p == 0).OnlyEnforceIf(bv1.Not())

# add solution
# model.AddBoolOr(bv1)
# model.AddBoolOr(bv2)
# model.AddBoolOr(bv3.Not())

status = ort.CpSolver().Solve(model)

if status == ort.INFEASIBLE:
    print("Model is UNSAT")
else:
    print("Model is not UNSAT")

Commenting in the # add solution bit result in the model becoming SAT!

[IgnaceBleukx]

OR-tools issue for the ones interested in following up:
google/or-tools#3643

[IgnaceBleukx]

Fixed in OR-tools main branch, not yet in pip version of library. Will be in version 9.6, closing issue when new OR-tools version is released in pip.