7 ms·
Constraint Solving with MiniZinc
- andrewflnr 8y agoCan anyone comment on the relative feasibility of using Z3 for problems of similar or greater scale? The performance is actually kind of concerning.
- Supersaiyan_IV 8y agoDepends on the search method, and heuristics employed, here's an excerpt from JaCoP constraint solver's documentation: http://jacopguide.osolpro.com/guideJaCoP.html#x1-730013 http://jacopguide.osolpro.com/guideJaCoP.html#x1-730013 The heuristics can be hierarchical permitting customized implementations, see 'IndomainHierarchical' here: http://jacopguide.osolpro.com/guideJaCoP.html#x1-820001 http://jacopguide.osolpro.com/guideJaCoP.html#x1-820001 What's interesting about JaCoP in particular is because it has derivative, and Multivariate Interval Newton Method constraints. If you can model your problem in terms of 'flow', you'll eliminate the risk of calculating beyond INT_MAX, in case that's a concern. Reference: http://jacopguide.osolpro.com/guideJaCoP.html#x1-490005 http://jacopguide.osolpro.com/guideJaCoP.html#x1-490005 And that's just JaCoP, there are many great constraint solvers out there.
- Supersaiyan_IV 8y agoFIY: MiniZinc is a high-level constraint programming system implemented by various constraint programming solvers. Here's the annual MiniZinc competition which ranks those constraint solvers: http://www.minizinc.org/challenge.html http://www.minizinc.org/challenge.html
- 3rdAccount 8y agoCan someone explain why I would use this instead of Python + Pulp or Pyomo, or Julia + JuMP.
- timClicks 8y agoPerhaps MiniZinc can be used in areas where linear programming is unable to model?
- bigger_cheese 8y agoI know my Work uses something called an SQP Solver (Sequential Quadratic Programming) for our nonlinear stuff I'm not sure how that compares.
- cerved 8y agoI don't know anything about those but Minizinc allows you to write one model that compiles to a SAT solver, MIP solver, CP solver, CBLS solver etc. Which is neat.
- wenc 8y agoI was going to write something but this answers your question. [1] pulp and jump only model mixed integer programs, if I’m not mistaken. However when I looked at this some years ago, I came across journal publications that found mixed integer program (MIP) solvers to be much faster than constraint solvers for many problems. I suspect that this was because MIP theory was much more well developed at the time and that commercial interests (airline scheduling, oil and gas, etc.) were driving impressive improvements in MIP solver technology (dominant players are IBM CPLEX, Gurobi and Xpress), whereas constraint programming remained more or less a niche domain in computer science. [1] https://www.solver.com/integer-constraint-programming https://www.solver.com/integer-constraint-programming
- 3rdAccount 8y agoPulp and Jump are interfaces to CBC, GUROBI, CPLEX, XPRESS...etc. They can do LP, MIP, IP, and Nonlinear optimization to a degree. These are used for massive scale optimization problems as you've indicated. When I look at constraint programming, it looks usable only for problems of a small fraction of my model's size I guess. It looks like the flatzinc language that minizinc compiles to has an interface to GUROBI, CPLEX, & CBC. So at least it can be used as a modeling language. Btw...Picat looks like it has similarities to Minizinc.
- mncharity 8y agoGiven the 2018 challenge results, I note OR-Tools is https://developers.google.com/optimization/ https://developers.google.com/optimization/ , its introduction is https://developers.google.com/optimization/introduction/overview https://developers.google.com/optimization/introduction/over... , and the Python version of getting started is https://developers.google.com/optimization/introduction/python https://developers.google.com/optimization/introduction/pyth... . There are an unofficial node.js bindings https://github.com/mapbox/node-or-tools https://github.com/mapbox/node-or-tools .
- Jtsummers 8y agoIf this is of interest to you, I can recommend the Coursera courses. They are very effective for introducing both MiniZinc and constraint-based modeling of problems.
- bazooka2th 8y agoIf you don't mind sharing, how do you use these tools?
- Jtsummers 8y agoI’ve used it for smaller problems ranging from toys and puzzles to small scale optimization and scheduling problems. In the latter, my biggest use was to prototype how I’d solve a problem for my sister in her job (scheduling facilities maintenance in a way that didn’t interfere with planned experiments and tests, what maintenance work could be done and when to minimize conflicts with customer schedules). It worked as an example but couldn’t handle the full factors (well, my laptop and lack of experience optimizing models) and they continued relying on (mostly) human judgement (worked out well enough). I also used it to make a soccer schedule. It worked better than my teammates attempt at making a scheduler from scratch (building both the solver and model). There are already systems for this that the league had available, it was more a “can I do this” challenge. More important, to me, was learning about a class of solvers and what problems they were effective at solving. Even though I have no immediate need it expanded my knowledge so I know where to start in the future rather than (foolishly) starting from scratch. Or I can point others to it. I’ve seen many devs (myself at times too) reinvent the wheel because we don’t know what options are out there. I took the course to combat that behavior in myself and to better guide colleagues, plus it was fun. (Apologies, on mobile. I have a few more paragraphs I could write but this is not the easiest entry mechanism for that.)
- bazooka2th 8y agoThanks for your reply! I asked because a couple years ago I started, but quickly quit, a Coursera optimization course.
- 8y ago
- jpnelson 8y agoI did some work with this a while ago to try and use MiniZinc to calculate genome edit distances, which was quite interesting: https://github.com/jpnelson/genome-edit https://github.com/jpnelson/genome-edit The hardest part is certainly making constraints that don't have any holes in them, and then making it fast. Making the MiniZinc solver faster than a search algorithm required a bit of knowledge about how the solver works. I can imagine there are some problems that are well suited to this, and this would be a good tool to solve them, but it's certainly not the best way to solve every problem (yet, anyway).
- ant6n 8y agoHow does this relate to using integer linear programming to solve linear constraint problems? Why would one use a dedicated language? When I model constraint satisfaction & optimization problems, I generally try to make linear models and define them using pulp in Python. The models are built by python programs; I feel using a dedicated domain-specific language is not so useful (you need general purpose computing to define problems, for example you need to read data that is necessary to build the model).
- 3rdAccount 8y agoI agree with you here. I think MiniZinc is more like a free/open-source version of the AIMMS modeling language, although AIMMS seems to have better I/O facilities.
- bash-j 8y agoHow do you optimise a delivery route with specific window times for each drop off using a linear model? How do you schedule shifts for employees to satisfy business requirements without also violating their contracts? How do you fill a truck with the right combinations of goods so that it maximises the space used, but also doesn't unbalance the container, and can still be unloaded at each drop off using first in last out? How do you maximise operating capacity at a factory when each time you change what you are building requires stop start time and you need to produce a range of products consistently, while also meeting customer delivery windows, and you don't have unlimited storage for inventory and limited staff with specific skills that only work certain hours or days of the week? How does a retailer layout their warehouses so when the orders for stores are picked it minimises the labour costs for not only picking the orders, but also putting stock on the shelves at the stores? How much should they order for each item, and how often do you deliver to stores? You can probably guess I work in Supply Chain.
- ant6n 8y agoI believe you're trying to make a point about something, but all I can see are (rethorical?) questions.
- skosch 8y agoHaving used Minizinc for a few years now, it's a great tool. Minizinc makes it easy to spell out a problem, try different ways to formulate the same constraint, and run the same model on some external data through lots of different solvers to see which one works best. It comes with an enormous constraint catalogue adapted to each solver. Whether you then use PuLP, OR-tools, JuMP etc. (or even Minizinc itself) for the actual implementation is up to you; but I've found that it is hard to beat when I am at the prototyping stage.
- 3rdAccount 8y agoAh, thanks for giving some context. Since I work in an industry that has our main problems being LP & MIP, I can see no reason to not use a general purpose language like Python or Julia to talk to an industrial solver like Gurobi. However, if I worked for a firm that did all sorts of optimization work (I'm jealous of anyone who does this), I might have to determine how best to formulate the problem and maybe MiniZinc is helpful there.
- prav 8y agoIs this in same category as OptaPlanner? How do these two compare?
- ge0ffrey 8y agoOptaPlanner (Apache license, 100% Java) is a constraint solver. MiniZinc (MPL, C++) is a modeling language for other constraint solvers. Both are used for similar use cases - Vehicle Routing Problem, employee rostering, task assignment, .... OptaPlanner uses metaheuristics and construction heuristics, java objects as input & output (not just arrays of integers and floating point numbers), constraints that can call any java code, supports multithreaded incremental solving, etc. It currently has no Minizinc adaptor or JSR-331 (a similar initiative) adaptor. If there's more demand for that, it would be considered.
- nuclx 8y agoI don't have many applications for constraint solving in my day-to-day work, but I genuinely think there is a need for a well-designed common language to express constraints on data sets - non-turing-complete, easy-to-use quantifiers etc. MiniZinc is that.
- tragomaskhalos 8y agoIn similar vein to others asking "how does this compare with ..."; I'm reading a book on Prolog at the moment and would be interested if anyone has experience in both MiniZinc and Prolog and can compare them for constraint solving ?
- phaedrus 8y agoI'm not familiar with MiniZinc and I've studied but not used Prolog; however I have worked on a library which combined a linear constraint solver with a Prolog-like DFS (depth first search) logic implementation. The most succinct difference is (usually) a constraint solver is going to find a solution (or the best solution) while a DFS logic will attempt to enumerate all solutions. For example, consider a geometric problem of placing a point on the plane according to constraints (such as left of line AB, above line CD, etc.) Assuming a solution exists, there might be a whole region of solutions (for example three lines might describe a triangle where any point inside the triangle is a solution). A linear constraint solver is going to give you an answer of an arbitrary point in the triangle. It is not going to give you a stream of results "1.00,5.00; 1.01,5.02; 1.02,5.04; etc." If you want that you need to perturb some of the inputs to the solver to change the output. In other words there is no built-in combinatoric enumeration order. In contrast, a depth first solver would output exactly that, because that's how it also views the problem internally - by enumerating options. It may be sophisticated in ruling out scanning parts of the space which can't be in the solution, but it can't avoid enumerating partial solutions which are part of a full solution because that's how the algorithm works. It would be the same as an implementation leaving arbitrary rows out of a table join in SQL - the algorithm depends, for correctness and completeness, on that not being done. (Note again the distinction between leaving out partial solutions that are part of a full solution versus leaving out searching entire regions which can be ruled out of ever being a solution. So I'm not arguing that it has to brute force solutions I'm making the more nuanced argument that the "row count" is significant in data flow within a DFS logic engine in a way that is not even a concept within a linear constraint solver's data flow. Or to put it another way, within a linear constraint solver there's only ever "one row" but it is kind of fuzzy what the values of the columns are.) However unlike a strictly linear constraint solver minizinc also supports either-or constraints so I don't know how much that changes the above. I would be interested to find out if MiniZinc tracks the combinatorics of multiple either-or constraints in the way that a Datalog or SQL would - I suspect it instead treats them all as interchangeable and indistinguishable rather than enumerable. Another difference between constraint solvers and DFS logic is generally you can pick an arbitrary variable in a constraint solver and change it's value an recalculate the model. In a DFS logic you generally cannot do that; at most you could (at the implementation level not the user level) unbind and rebind the most recently bound variable, or unwind the stack and recalculate from an earlier point.
- sevensor 8y agoI highly recommend clicking through to the second post in the series. It discusses optimizing the models -- an area where I've had some success and a lot of failure. There are some really complicated tradeoffs to be managed, and it can be incredibly hard to measure whether you've made a genuine optimization or whether you've accidentally tipped the solver into a happy path for one particular instance of the problem you're trying to solve. Some solvers use PRNGs, and you have to be careful to try enough seeds to get a clear picture of the solver's performance. This can be challenging when the time to solution is exponentially distributed with a mean of several hours. The most important thing OP does, in my opinion, is to solve a smaller (but not otherwise simpler) version of the problem. This is crucial if you're going to find a tractable representation -- or rather, if you're going to eliminate completely bogus representations of the problem.
- mindcrime 8y agoFYI, there is a small mini-zinc community at the corresponding sub-reddit: https://www.reddit.com/r/MiniZinc/ https://www.reddit.com/r/MiniZinc/