Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some MiniZinc subsolvers give wrongly an unsatisfiable on a specific input file #160

Closed
rubenkindt opened this issue Nov 15, 2022 · 2 comments

Comments

@rubenkindt
Copy link

rubenkindt commented Nov 15, 2022

solver: Minizinc's subsolvers minizinc:float, minizinc:coinbc, minizinc:mip, minizinc:osicbc
CPMpy: version v0.9.9 commit e79b3af
minizinc-python release version 0.7.0 commit {MiniZinc/minizinc-python@a195cf6)

Some MiniZinc solvers did not complain about an "alldifferent()" in the problem but did give a UNSATISFIABLE with a runtime or 0 sec. Unfortunately, I could not remove any constraint from the original file even a shuffle of the constraints turns the problem into a feasible one.

original.zip

from cpmpy import *

file = "original" # don't forget to unzip
m = Model().from_file(file)
m.solve(solver="minizinc:mip") # same with osicbc, float, coinbc
print(m.status())

expected behavior:
That the mip solver complains about the 'alldifferent()' constraint in the problem or give any other status different from UNSATISFIABLE, since the correct solution is optimal.

bug found while working on my master thesis.
Edits: better title, added the shuffle sentence, changed "minimized" to "original" and added used minizinc-python version

@rubenkindt rubenkindt changed the title Minizinc subsolvers did not complain about global functions and gave UNSATISFIABLE Some MiniZinc subsolvers give wrongly an unsatisfiable on a specific input file Nov 15, 2022
@rubenkindt
Copy link
Author

Looking at what

from cpmpy.transformations.get_variables import get_variables, get_variables_model
for i in get_variables_model(m):
    print(i + ".lb="+str(i.lb) +",ub="+str(i.ub)+"name="+str(i.name))

produces, this bug most likely is the same one as issues #96 and #164. This could be fixed by pull #179

@JoD JoD added the fuzz-test label Mar 27, 2023
@Wout4
Copy link
Collaborator

Wout4 commented Jun 30, 2023

this is indeed a bounds issue with minizinc, we check for that now and throw an error

@Wout4 Wout4 closed this as completed Jun 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants