MiniZinc
minizinc.org
minizinc.org
My takeaway: modeling problems in minizinc correctly is exceptionally difficult for non-trivial problems. You can model it correctly, but you'll likely still need to add additional "constraints" that improve the performance of the solver to the degree where it's even remotely usable to solve real problems.
It's a really interesting tool, but one of the reasons we thought it might be useful for this problem is so that non-technical people could easily change the constraints and play with the costs for different operations. I don't think it's particularly good for that, at least in this problem domain.
key takeaway: Boisot and McKelvey updated this law to the "law of requisite complexity", that holds that, in order to be efficaciously adaptive, the internal complexity of a system must match the external complexity it confronts.
Once you added domain-specific performance-oriented constraints, did you find this to be a useful and viable approach to the problem?
It worked quite well for the more trivial rules, but as I added more complex rules, it wouldn't solve within reasonable time.
Unfortunately I didn't really figure out how to direct the solver in way that would speed up things.
I find the outputs command of MiniZinc particularly counter-intuitive and hard to use.
But one of its drawbacks is its limitation of handling input and output (including preprocessing and postprocessing). In some cases - for example when the output is rather simple - I use for example Picat/Python to transform input to MiniZinc format (.dzn format or JSON) and then run MiniZinc.
But for more fancy output I tend to use Picat or Python + (OR-tools CP/SAT or CPMpy or minizinc-python).
That being said, one can do fancier output in MiniZinc, though it requires some work. Here is a model for certain scheduling problems which exemplifies this: http://hakank.org/minizinc/scheduling_with_assignments.mzn . But the output was a little easier to do in Picat: http://hakank.org/picat/scheduling_with_assignments.pi
And a person I didn't know posted a solution using MiniZinc. That person happens to also be on HN, so whenever constraint programming comes up, or MiniZinc, I post this story, and Hakan shows up. You around, Hakan? :-)
Here's Hakan's page on the solution: http://www.hakank.org/minizinc/einav_puzzle.mzn
For the comments referring to examples more complex than Sudoku, his website is the best that I have found! Thanks Hakan.
Of course! :-)
Only after it makes sense to take https://www.coursera.org/learn/basic-modeling and https://www.coursera.org/learn/advanced-modeling courses.
If you want a quick start read really good tutorial on official website https://www.minizinc.org/doc-2.7.2/en/part_2_tutorial.html and play with examples at online playground https://play.disopt.com/ or locally installing MiniZincIDE.
We used it to create models of networked biological systems (e.g. the immune system, gene regulatory networks, etc.). The network topology was constructed from mined academic literature and then the model was constrained using data. The great thing about using MiniZinc was that it could propose multiple models with the same or similar “accuracy” to the data. You would then have an ensemble of models from which to make predictions (i.e. how does a drug affect the system).
We would have MiniZinc files that were 10s or 100s of MBs and would run for days. Sometimes they would be unsatisfiable within a few seconds, other times within hours. Many of the solvers are single threaded, and those that are multithreaded don’t seem to be much more efficient with more cores.
MiniZinc is very difficult to debug and the paradigm shift can be jarring coming from procedural languages. However, I am grateful it exists and for the work that many have put into it. Similar to the train yard comment, we used Python to construct the MiniZinc models and then submitted them to the solvers via the minizinc-python package which is well written and meek maintained.
* a certain aspect ratio,
* rotational symmetry,
* no spots where four corners touch,
and a few other ad-hoc constraints that I can't remember exactly, to exclude certain sub-patterns.
I'm at the very early planning (read: daydreaming ;) stage for a tiling project of my own, (where my "constraints" are "has to be nerdy-awesome"). Like find a specific conway's game of life still life, or perhaps use the newly discovered aperiodic "hat" tileing.
Any chance you would be willing to dump your notes somewhere I can see?
Another approach to the constraints could be to define the set of covered subsquares for each placement, and have a single constraint that says that each subsquare must be covered exactly once.
It was a pretty small patio (about 2 by 3 meters), with 17 square tiles and 12 rectangle tiles, and this formulation worked well enough to find all solutions to that in reasonable time. However, you get a lot of minor variations on the same general pattern. On this small scale just quickly scrolling these variations was manageable, but with a larger project you'd have to do something more intelligent.
I enjoyed the courses and learning the techniques through the exercises but I still haven't really found a good application to a problem I need to solve for work or side projects.
I then used MiniZinc to solve a resource allocation problem for two large border checkpoints, assigning staff across lanes for multiple transit types (motorcycle, car, truck, bus and train).
Constraint Solving with MiniZinc - https://news.ycombinator.com/item?id=18161145 - Oct 2018 (38 comments)
MiniZinc: free and open-source constraint modeling language - https://news.ycombinator.com/item?id=16194112 - Jan 2018 (33 comments)
Solving Problems with MiniZinc - https://news.ycombinator.com/item?id=15530630 - Oct 2017 (15 comments)
Problem Solving with MiniZinc - https://news.ycombinator.com/item?id=14062281 - April 2017 (1 comment)
Clojure to MiniZinc - https://news.ycombinator.com/item?id=10042958 - Aug 2015 (4 comments)
Constraint programming and The MiniZinc Challenge (2013) - https://news.ycombinator.com/item?id=7863946 - June 2014 (1 comment)
Maybe it's just that formally expressing a set of constraints doesn't come naturally to me. I'm sure with a lot of practice, writing MiniZinc code would be easier.
The Google OR-Tools Python API also might be easier if you're generating models dynamically. I wouldn't want to generate MiniZinc code...
The goal of an heuristic algorithm is to produce a near-optimal or approximate solution in a reasonable amount of time. From here, some heuristics have more or less theory behind them and that theory shows what sort of properties the solution has.
[1] https://optimization.cbe.cornell.edu/index.php?title=Heurist...
[2] https://en.wikipedia.org/wiki/Heuristic_(computer_science)
I've used MiniZinc too (in a different project), where I wanted some optimal results to compare against some heuristic algorithms I was developing. MiniZinc requires more careful thought when it comes to encoding/representing the problem (i.e. sets of integers, rather than familiar Java objects), but it's not too difficult. Since it's optimal it can take an age to run; I could only scale my problem up to N=11 before it was taking more than 24 hours (that was enough for my comparisons though)
I think the fact that it is written for the JVM is especially helpful because you can write constraints using JVM libraries, which are a massive boon in some of the very domain specific areas that I’ve worked in. Writing geospatial or RF propagation constraints in a DSL like minizinc is a total nonstarter.
Adoption for these systems might be higher if they had a more readable syntax (and bonus if they could transpile down to source code you can tweak)
Also maybe I missed it on mobile, but I would love examples of the syntax and examples of application usage on the first page. Maybe this is useful to me! Who knows? That information should be easy to find
The minizinc code looks pretty reasonable to me though. Specify your variables as ranges. Specify your constraints as math equations. Tell it what you’re looking to maximise / minimise.
https://www.minizinc.org/doc-2.7.6/en/modelling.html#ex-cake...
Why does everything need to look like JavaScript in order for Average Joe programmer to be able to read it?
But I can’t use OCaml or Coq at work.
I can use typescript. I can use algebraic data types, well typed functional combinators, exhaustive switch statements (through linter) and other functional design patterns.
I’d like to be able to use formal proofs. If it means dumbed down version that average joe can work with that can gain wider adoption - that’s much better situation to be in than not having anything at all.
There must be more developers in similar situation.
I developed and deployed a rail yard scheduling application based on MiniZinc which is being used daily in production at several sites by one of the largest rail network operators in Australia.
Like others here I had started out with the free coursera courses a couple of years prior and was really taken by the declarative nature of the language. When approached about the yard scheduling problem I thought it seemed like a good fit and was able to quickly generate a proof of concept. I spent the next 2 years iterating on it until it was able to handle all of the real world (and real-time) constraints.
The topology: - A yard has many tracks (~40 in our largest case) - A track has many track circuits (this reflects the underyling control system) - ~ 250 track circuits - A circuit can only be occupied by 1 train at a time - A train occupies many track circuits - This yard was a staging point for 2 unloading locations - Each unloading location had many loaders
The dynamics: - Trains entered the yard primarily for the purpose of proceeding to the unload and unloading - Most trains required 'provisioning' on certain tracks before or after unloading - Some trains required' shunting', making or breaking a consist into separate peices for repair or reconfiguration - Some trains required manual examination, meaning adjacent tracks must be vacant while the inspection took place - There are many routes trains can take (we pre-calculated these) - There were multiple train operators using the yard - Each operator had soft or hard constraints on where and how they would like their trains to operate - The primary objective function was meeting the agreed unloading time at the port and completing all maintenance and inspections - Secondary objectives were queuing times, route preferences
The implementation: - ~50k python codebase - Data read from 4 internal systems for maintenance requirements, schedules, etc - Telemetry from the train control system used to determine train location within the yard - Data was stored in python using attrs, cattrs and roundtripped to JSON - MiniZinc models were compiled on demand, this was a massive help in performance and flexibility - Frontend was a Streamlit app which displayed schedules using Altair/Vega-lite - The core 'solve' method was used in a variety of ways, you could reschedule a single trains, or many trains at once (the ideal), or a heuristic where trains were scheduled in dynamic batches (required for longer +24hr runs) - The frontend exposed a '1 click schedulers' which would bring in all the data and produce a feasible schedule very quickly (<1min) with a heuristic - Once the business was confident in the tool we had it running inside a container on an hourly basis to continually produce optimal schedules based on the latest available data which was the advertised to operators - Used Google OR-Tools as the backend solver which was by far the fastest - Trains were scheduled using 1minute time blocks
Reflection: This was an extremely challenging project for a lot of reasons, mainly because I was a 1 man team and trying to learn on a deadline, also this was during covid and I had nothing else to do so it became quite all consuming. I have since thought that if I could do it all again would the approach be different?
Of all the parts of the tech stack I enjoyed MiniZinc the most and would happily use it again. Modelling with constraints is not easy but there is a rock solid gaurantee that comes with it that pleases me greatly. As other people have said there is a lack of intermediate or advanced level "real world" tutorials which I completely agree with and am working on in my spare time.
I would say that things got a lot easier once I stopped trying to represent the entire model ahead of time in one minizinc file, and instead compiled models as required from the python side based on the data I was dealing with.
Python was great for the POC stage and horrendous once it got to a certain size. Alas a rewrite was never in the cards. We dealt with it by using type hints everywhere
Streamlit is absolutely not fit for purpose for anything beyond hello-world, at least at the time I was using it. Unfortunately I had no experience in frontends at all and just needed a way to expose the model to end users and display results so we made it work.
Altair/Vega-lite is a fantastic charting library which I would readily use again. Being able to produce standalone gantt-style train schedules complete with interaction was a major win for both end users and myself for debugging.
I have to duck off but love talking about this stuff, you can reach me at "justin dot rawlings at protonmail dot com" or jmjrawlings on github.
The model was in user-acceptance testing phase for almost a year until it was feature complete, had acceptable performance, was verified by the controllers etc.
I should clarify that the model was not in charge of actually telling trains where to go. Train Controllers are solely responsible for that and do so using a Train Control System which has rigorous safety measures in place to ensure collisions do not happen.
The model was a decision support system for the controllers. It showed them how they could best run the yard given the current state of play and expected arrivals. Controllers were absolutely free to disregard the advice which certainly happened earlier on but as the model got better and better this became less of an issue.
I should say the main reason I could 'speak the same language' with the end users in this case is due to the vega-lite schedule visualisation. Every single part of the constraint model (trains, tracks, tasks, track failures, even the objective function) had an analagous visual representation on the diagram which meant controllers both confident the model did what I said it did, and they could also easily point out errors by referring to the diagram.
A big feature of this model was that there was essentially 0 abstraction over what was happening in the real world. The model took inputs from all of the exact same systems that train controllers used, and produced results that tied directly back to the track circuits of the train control system. This meant that we could view historical yard performance, current yard state, and future optimised schedule all on the same diagram which was so great for debugging and verification.
One thing I really wish there was more of though, was motivating examples that make sense in my world.
The comment "I used minizinc to try and generate levels for my puzzle game by encoding the rules." is a decent example.
I'll believe that sat-solvers are getting better and should be used more, but I feel there's a real dearth of motivating examples for those of us who live, eat, breathe and have no problem with the C/C++/systems engineering/high performance stuff. :)
edit:
Basically, I want a few dozen well written examples of things like (starting from "Solving Sudoku with SAT"):
https://codingnest.com/modern-sat-solvers-fast-neat-underuse...
It seems a significant amount of cleverness is required to model rules as the equations, before passing them off to the solver.
Can I specify a list of statements, constraints, prioritisations and the have it solve it for the best possible solution? Is that it? If so, I need it to figure out my optimal workout schedule given a handful of constraints (a problem I’ve been thinking about since I started university twenty years ago :) )
> Can I specify a list of statements, constraints, prioritisations and the have it solve it for the best possible solution? Is that it? If so, I need it to figure out my optimal workout schedule given a handful of constraints (a problem I’ve been thinking about since I started university twenty years ago :) )
Yes!
Large companies (think any of the Global 2000) benefit from a couple % improvement on their operations that lead to many $M in savings.
Sophisticated programming languages dive towards this direction already compared to untyped cousins. Programs are validated against type theory correctness. You can go deeper with dependent types. And those languages go all the way down to prove everything there is to be proven.
Physical design systems (modeling possible boat hulls, say—not the physics itself but the interaction of numerous variables) and resource allocation (drafting a baseball team, say) seem like other likely areas, though I’ve got no idea if constraint tools are the best option or whether they’re even used.
Broadly: if a multivariate problem can’t be modeled, a constraint-based search strategy is the(/one) next-best tool.
I don't think MiniZinc itself is used by any package-management tools, although some use competing tools/libraries. Personally I've used MiniZinc for a related problem: finding a subset of dependencies (of a given size, say 10), which satisfy the most outputs.
Edit: Another constraint modelling problem I've tackled (although I didn't use MiniZinc to solve it) is seating allocation on public transport: if the scheduled vehicle is unavailable, and the replacement has a different seating layout, how can we best assign the reserved seats (taking into account ticket class, seat direction, window/aisle, amenities, etc.)?
MiniZinc is a free and open-source constraint modeling language.
You can use MiniZinc to model constraint satisfaction and optimization problems in a high-level, solver-independent way, taking advantage of a large library of pre-defined constraints. Your model is then compiled into FlatZinc, a solver input language that is understood by a wide range of solvers.