4 ms·

Thanks for the suggestion! I've known we should be submitting our verification problems to smtcomp, but hadn't thought about minizinc challenges Our current mo

Thanks for the suggestion! I've known we should be submitting our verification problems to smtcomp, but hadn't thought about minizinc challenges Our current model is here https://github.com/draperlaboratory/VIBES/blob/main/resources/minizinc/model.mzn https://github.com/draperlaboratory/VIBES/blob/main/resource... We don't have any parameter files committed to the repo, they are generated by the compiler. It has been on my todo list for a while to completely refactor this model. Currently, the constraint solve can take 10s on our hardest problems so far, which would be nice to get down, but not our biggest blocker.

mzl 4y ago
Thanks, and nice to see! Even if 10 seconds is often fast enough for solving a problem, I can imagine that it would be good to get down. From the code I guess that you use Chuffed, have you also tested other solvers? OR-Tools with parallel solving feels like the standard thing to try. I can also imagine that the time will start to go up significantly if larger patches are specified, but perhaps that is not a very common use-case. Having some example instances for ease of testing would be fun, and make it easier for a drive-by constraint programmer to try it out. Hoping to see it in the competition next year. Problems that are mostly reasonably fast to solve can still be interesting IMHO, especially when they are probably only fast because some solvers (Chuffed/OR-Tools) have very good automatic heuristics.