[HN Gopher] MiniZinc
___________________________________________________________________
MiniZinc
Author : gavi
Score : 131 points
Date : 2023-07-21 18:32 UTC (4 hours ago)
(HTM) web link (www.minizinc.org)
(TXT) w3m dump (www.minizinc.org)
| surfsvammel wrote:
| 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 :) )
| cjalmeida wrote:
| At work, a large consulting company, we use constraint
| programming 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.
| nextaccountic wrote:
| 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!
| max_ wrote:
| What exactly is "constraint modeling" and what is it used for?
| jononor wrote:
| 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.
| orbit7 wrote:
| 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!
| maleldil wrote:
| I don't get people posting GPT answers. If parent wanted
| that, surely they would've done that themselves?
| ashish01 wrote:
| Let Me GPT That For You! -> https://gprivate.com/65ubk
| sudokupuzzler wrote:
| Solving sudoku and other kinds of logical "puzzles".
| mirekrusin wrote:
| 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.
| chriswarbo wrote:
| 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.)?
| GavinMcG wrote:
| 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.
| TimTheTinker wrote:
| 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...
| wsdookadr wrote:
| 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)
| chriswarbo wrote:
| 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)
| colonwqbang wrote:
| 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.
| ShadowBanThis01 wrote:
| You forgot to tell us what it is.
| WJW wrote:
| You forgot to look up the trivially googleable term (or to read
| TFA) before deciding to post.
| xtagon wrote:
| 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._
| jpnelson wrote:
| I wrote a thesis on using constraint satisfaction with minizinc
| to solve the genome edit distance problem:
| https://github.com/jpnelson/genome-edit/blob/master/thesis.p...
|
| 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.
| jomoho wrote:
| 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.
| aidos wrote:
| Is that a minizinc thing or a solver thing in general?
| shaunxcode wrote:
| 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.
| 0cf8612b2e1e wrote:
| 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.
| zellyn wrote:
| 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?
| sirwhinesalot wrote:
| 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)...
| wjnc wrote:
| 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).
| mattnewport wrote:
| 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.
| froggychairs wrote:
| 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
| mirekrusin wrote:
| Yes exactly, we need typescript style solution to get best 80%
| of ocaml/haskell available to joes kind of thing.
| aidos wrote:
| 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...
| dang wrote:
| 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)
| ChrisArchitect wrote:
| Anything new here?
| ChrisArchitect wrote:
| Some previous discussion from 2018:
|
| https://news.ycombinator.com/item?id=16194112
___________________________________________________________________
(page generated 2023-07-21 23:00 UTC)