MiniZinc(minizinc.org)
minizinc.org
MiniZinc
https://www.minizinc.org/
75 comments
I used minizinc to try and generate levels for my puzzle game by encoding the rules.
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.
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.
Do I understand correctly that this kind of constraint satisfaction is more complex than just turning things into a bunch of SAT clauses? Otherwise (and admittedly without a deep understanding of genomics or solvers), I would be surprised if constraint satisfaction were the best approach for edit distance…
Once you added domain-specific performance-oriented constraints, did you find this to be a useful and viable approach to the problem?
Once you added domain-specific performance-oriented constraints, did you find this to be a useful and viable approach to the problem?
MiniZinc is just a modeling language, you can throw the problem at different solvers. You can use SAT solvers (assuming you have some wrapper that translates FlatZinc to CNF), CP solvers (can be SAT-based underneath or use different algorithms like MAC), SMT solvers (SAT Modulo Theories like Arithmetic), MIP solvers (usually Simplex + Branch & Bound)...
Is that a minizinc thing or a solver thing in general?
https://en.wikipedia.org/wiki/Variety_(cybernetics)
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.
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.
“Inner platform effect”
I have only ever used Z3, but you might be onto something. Modeling problems is really challenging. It does not help that if you search for documentation or guidance there one two types of resources: beginner Sudoku or primary literature academic papers discussing the minutia of optimization properties with so much jargon.
How is MiniZinc in this aspect compared to Picat or other constraints solving languages?
I find the outputs command of MiniZinc particularly counter-intuitive and hard to use.
I find the outputs command of MiniZinc particularly counter-intuitive and hard to use.
I really like MiniZinc, especially that one can test a lot of different type of solvers for a problem.
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
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
Whenever MiniZinc, or constraint programming, comes up, I post this link to a programming challenge a friend gave me...14 years ago. I was learning J, and the challenge was me in J, her in javascript or php (she never completed the solution). Here's the link: https://gcanyon.wordpress.com/2009/10/28/a-programming-puzzl...
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
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
I have a secret obsession with hakank’s constraint programming solutions. One of the things that is difficult with constraint programming is that there are several dozens of solvers out there, and they all have different capabilities and limitations. There have been a bunch of times that I have gotten stuck modeling a problem, find some similar problems with brilliant solutions on hakank’s page, and then realize I should actually be using a different solver or a different language.
> You around, Hakan? :-)
Of course! :-)
Of course! :-)
MiniZinc is high-level modeling language, before using it I'd suggest taking course https://www.coursera.org/learn/discrete-optimization where you could use/create different solvers.
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.
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.
I used MiniZinc extensively in my previous position, and have mixed feelings about it. As is stated in other comments, it works very well for specific small problems, but when the model gets complex it can become unwieldy.
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.
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.
As a not professional programmer, but mathematically inclined I can say I found modelling in MiniZinc crazily hard. I tried the Coursera class, put in the hours and failed. It took me back to some classes where everything I tried failed and the proper result felt so near what I was trying that it was hard to digest a better strategy the next time. It did give me a new feeling for complexity and model space reduction. Somewhere MiniZinc and other engines are super efficient, you just need to put the problem in the right form (and therein lies the catch).
I took a class in grad school where MiniZinc was our go-to to solve many different problems and I had the same issue. I found that the handbook[1] was pretty helpful in modeling tricks and understanding the logic where I was used to CPLEX modeling style and Python OR-Tools.
[1] https://www.minizinc.org/doc-2.5.5/en/index.html
[1] https://www.minizinc.org/doc-2.5.5/en/index.html
Can LLM help in this task?
I'm not an expert on MiniZinc, but tried applying it and GPT-4 to a toy problem: https://buttondown.email/aostiles/archive/flight-optimizatio...
Seems like no? I mean, they are great in getting some text that looks correct but is an hallucination. LLM can help in getting something roughly ok, that a human can fix. This doesn't seem to be the case here.
Translating is the thing that GPT is best at. Hallucination is much less of a problem here because you’re dealing with a whole language, not a ton of libraries with different APIs.
I used Minizinc to come up with tiling patterns for a patio. I had m 2x2 tiles and n 3x2 tiles and wrote a model to generate patterns that had:
* 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.
* 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.
That sounds super cool!
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?
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?
I used a pretty straightforward formulation, with a binary decision variable for each possible tile placement/orientation, and constraints to ensure that the pattern is possible to build: uses correct number of tiles of each type, no overlap ("if there's a 2x2 tile at (x,y), there is no 2x2 tile at (x,y+1)").
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.
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.
do you have a pic of the result?
I should have, but wasn't able to find any right now. This is what the pattern looks like, at least: https://imgur.com/a/WpbxDNu
I can recommend this course and its sequels on Coursera to anyone interested in learning MiniZinc: https://www.coursera.org/learn/basic-modeling
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 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.
Yes, the best online courses I have ever taken: entertaining and challenging in equal measure.
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).
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).
Related:
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)
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)
I once tried to use MiniZinc as a back-end for a school timetabling app I was working on, and came away with the impression that the OptaPlanner Java API would be a lot easier to use. (Although unlike solvers, OptaPlanner uses heuristic algorithms -- simulated annealing, etc.)
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...
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...
I've used OptaPlanner in production, it was pretty straightforward and coped perfectly well with the few-hundred-variable problems we needed it for (we ran it with a timeout, and its solutions were good). If you're comfortable programming Java, it should be easy enough (note that it relies on mutating objects in-place; which took some getting used to since I was using it from Scala!)
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'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)
That an algorithm is heuristic does not preclude it from being provably correct.
It precludes it from being optimal!
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)
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 have actually found that optaplanner often gets better results on hard problems than a lot of constraint solvers do. Part of that has to do with a genius aspect of how it was designed: constraint evaluation is built on top of the drools rule engine algorithm (an evolution of the Rete algorithm).
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.
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.
OptaPlanner was forked as Timefold by the team behind it:
https://timefold.ai/blog/2023/optaplanner-fork/
We made it twice as fast (by replacing Drools).
Thanks for the note! This is helpful to know.
Im sure this is useful but these languages (proof langs, constraints, etc) are always so difficult to parse or read
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
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
I’ve played with minizinc in the past though we use scipopt now instead.
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...
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...
Judging from this particular example, it doesn't look a lot different than more established optimization software like CVXPY, no?
https://www.cvxpy.org/examples/basic/linear_program.html
https://www.cvxpy.org/examples/basic/linear_program.html
Yes exactly, we need typescript style solution to get best 80% of ocaml/haskell available to joes kind of thing.
Do you not find this idea somewhat embarrassing?
Why does everything need to look like JavaScript in order for Average Joe programmer to be able to read it?
Why does everything need to look like JavaScript in order for Average Joe programmer to be able to read it?
It absolutely doesn’t.
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.
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.
My goodness, a HN topic I can speak on with some level of expertise!
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.
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.
How can you be sure that your constraint model is correct? When the models are so complex that seems like a real challenge! In your case was it possible to take a proposed solution and verify that it does not have any issues? Are there many other safeguards in place to prevent train collisions or invalid schedules?
Fortunately the colleague who proposed this project was a former train controller with encyclopaedic knowledge of the particular yard and its operations. You find that all of these experienced train controllers can just look at a schedule and instantly tell you if it's viable or not. This was a really important part of development because I had rapid feedback and could prioritise the features that were really important to the people on the ground.
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.
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.
This sounds like an amazing project. Thank you very much for sharing it here. You should be proud! Few people can really point to a project and say "people use this and its a genuine improvement." The world needs more people like you!
Thanks for sharing this fascinating tale!
These things look neat! I can tell, being in the engineering industry for 20+ years that there's a lot of excitement and progress happening.
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.
(also: https://news.ycombinator.com/item?id=36087464)
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.
(also: https://news.ycombinator.com/item?id=36087464)
Constraint modelling is really neat. It only works well on a specific category of problems, but when it works it can feel almost like cheating. You don't actually do anything, you just restate the problem in code and the computer does the work for you.
Forgive my ignorance, but what kinds of problems are constraint solving good for?
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 :) )
GUI layout can be done by solving constraints, like in Cassowary, which is used in iOS and has implementations in many languages
> 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!
> 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!
At work, a large consulting company, we use constraint programming (actually, mostly mixed integer prog and meta heuristics) to solve problems in logistics scheduling, route optimization, staff assignment, production planning, marketing (pricing, store assortment) finance (portfolio, capital budgeting) and others.
Large companies (think any of the Global 2000) benefit from a couple % improvement on their operations that lead to many $M in savings.
Large companies (think any of the Global 2000) benefit from a couple % improvement on their operations that lead to many $M in savings.
Scheduling problems are a very well established domain for constraint programming, you’d very likely find it easier to express and solve your problem than with other methods.
How does this kind of constraint modeling compare with logic based approaches like Answer Set Programming (https://potassco.org)? Years ago, I got excited by the possibilities of ASP but it does not seem to have progressed much
Constraint programming with MiniZinc is great for some problems. There is a good Coursera class on MiniZinc. I also had a simple Python+MiniZinc example in my last Python book.
This is how you write a proper title: https://news.ycombinator.com/item?id=16194112
What exactly is "constraint modeling" and what is it used for?
Scheduling is probably the most obvious example of a real problem. You’ve got a space that has many different ways of being bounded and need to efficiently search that space.
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.
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've wanted to do this myself... Tho as both an armchair engineer and an armchair programmer. If I'd gotten through engineering in university, (and studied programming language design) this would be an utterly tempting idea for me to try. I must have come back to thinking about doing this ten times in the last fifteen years or so. Off the top of my head, scientific models also sound like they might fit with constraint modelling, tho I might be far too superficial in my understanding of both subjects there.
Dependency management is a common example; e.g. we want A; A depends on B and C; B depends on D or E; C conflicts with D; etc. These are all constraints, and we can ask a system like MiniZinc to find a set of packages which don't conflict (in that example {A, B, C, E} satisfy the constraints).
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.)?
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.)?
Examples from the software domain:
Dependency resolution in package managers (packages with version requirements) may use constraint solving.
Or type checking may be implemented using constraint solving.
Though often if the application is well understood enough, it may jump over generic modelling language like MiniZinc and generate instructions for a boolean satisfaction solver directly.
Solving sudoku and other kinds of logical "puzzles".
Provable properties for cryptographic algorithms is a thing. Provably correct compilers exist. It’s not hard to imagine provably correct kernel modules for example and benefits they’d bring. If they had better ux you could imagine business logic, state machines, asynchronous computation to have provable properties as well. It’s very interesting area but on the edge of usability currently. I’d predict it has great future as ai gets incorporated more and more as it gives solid logic/mathematical proofs over solutions - if it doesn’t make sense to you, think json schema like validated llm output but for any computation.
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.
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.
Let Me GPT That For You! -> https://gprivate.com/65ubk
My GPT answer was: Imagine you have a big box of colorful building blocks, and you want to create something specific, like a house or a car. But you have some rules or constraints that you need to follow in order to complete your creation. Constraint modeling is like playing with those building blocks, but with rules. It helps you figure out how to build something while following certain restrictions. These restrictions could be things like the size or shape of the blocks you can use, how they can fit together, or even how many blocks you have to use. So, constraint modeling is like a game where you have to solve puzzles using your building blocks, but you have to follow certain rules to complete the puzzle. It helps you think logically and creatively to build something amazing!
I don't get people posting GPT answers. If parent wanted that, surely they would've done that themselves?
Someone else at the time had posted a let me GPT that response to someone's question which for me provided a very unclear response, I was re-prompting to get a more simplified explanation and it gave something that seemed helpful to me, so also to the question raised, no one else at the time had otherwise answered. I don't generally use GPT responses in comments hence why I noted in this case it was a GPT response and not my own.
Anything new here?
Some previous discussion from 2018:
https://news.ycombinator.com/item?id=16194112
https://news.ycombinator.com/item?id=16194112
You forgot to tell us what it is.
The first two paragraphs of the home page say what it is:
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.
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.
You forgot to look up the trivially googleable term (or to read TFA) before deciding to post.
You forgot to muster up some self-respect and demand better.
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.