Parameters to Exact

[IgnaceBleukx]

When using the Exact solver, it seems some things go wrong when translating the arguments. I'm not sure whether this is due to CPMpy or the Python interface of Exact itself, maybe @JoD can help here.

I have the following unsat Sudoku model:

import cpmpy as cp
import numpy as np
e = 0
given = np.array([
    [e, e, e,  2, e, 5,  e, e, e],
    [e, 9, e,  e, e, e,  7, 3, e],
    [e, e, 2,  e, e, 9,  e, 6, e],

    [2, e, 1,  e, e, e,  4, e, 9],
    [e, e, e,  e, 7, e,  e, e, e],
    [6, e, 9,  e, e, e,  e, e, 1],

    [e, 8, e,  4, e, e,  1, e, e],
    [e, 6, 3,  e, e, e,  e, 8, e],
    [e, e, e,  6, e, 8,  e, e, e]])

# make the model
cells = cp.intvar(1,9,shape=(9,9),name="cells")

m = cp.Model()
m += [cp.AllDifferent(row) for row in cells]
m += [cp.AllDifferent(col) for col in cells.T]

for i in range(0,9,3):
    for j in range(0,9,3):
        m += cp.AllDifferent(cells[i:i+3, j:j+3])
m += cells[given != 0] == given[given != 0]

print(m.solve(solver="exact"))
>>False

Now, I would like a proof-log as to why this is UNSAT. I should be able to do:

s = cp.SolverLookup.get("exact", m)
s.solve(verbosity=10, **{"proof-log": "path/to/proof"})

But the output printed by Exact is:

c #vars 2511 #constraints 1337
c PRESOLVE

Also, when trying other arguments like print-opb no extra output is given.

[JoD]

I think this is due to Exact. And I think it's solved in the new version. Now to just get the PyPi package updated again...

Will work on this PyPi package next week.

[IgnaceBleukx]

Okay thanks! Is there a branch I can build from source from that has this issue resolved already?