mzl

7 ms·

61.
by mzl 1y ago
Very nice project. Do you have some statistics for how long it takes to solve the harder instances for different solvers? One thing to note for that, is that I saw the default parallelism of 4 in the run file. OR-Tools CP-SAT works best if
62.
AI chip firm Cerebras raises $1.1B(finance.yahoo.com)
1 points by mzl 1y ago|0 comments
63.
by mzl 1y ago
When using minizinc or other constraint programming tools to solve puzzles that require a single solution, I typically run them asking for 2 solutions. If I get 1 solution only, I know the puzzle is well formed, if I get more than one solut
64.
by mzl 1y ago
Any tool that can solver hard problems will also have non-trivial runtime behavior. That is an unfortunate fact. But you are also correct in that combinatorial optimizaton solvers (CP, SAT, SMT, MIP, ...) often have quite sharp edges that a
65.
by mzl 1y ago
I would say that for the specific use-case of a modeling layer for something like constraint programming, SMT, or MIP, full operator overloading is superior. I've written such layers in many languages and used them in even more languag
66.
by mzl 1y ago
If you want to work in Python, I would either use OR-Tools which has a Python library or CPMpy which is a solver agnostic Python library using numpy style for modeling combinatorial optimization problems. There is a Python package for MiniZ
67.
by mzl 1y ago
One missing thing in Rust is that the comparison operators are hard-coded to return bool values, which means that it is not possible to build up full expression trees form normal code using operator overloading. Thus the need for functions
68.
by mzl 1y ago
Has there been any published example of where this solver outperforms a classical solver?
69.
by mzl 1y ago
Manual verification of releases and chain-of-trust systems help a lot. See for example https://lucumr.pocoo.org/2019/7/29/dependency-scaling/
70.
by mzl 1y ago
The MiniZinc Coursera courses ( https://www.minizinc.org/resources/#courses-title ) are useful to get a good basis for understanding constraint programming. It’s not a fast solution being full courses, but it is a very g
71.
by mzl 1y ago
I get what you are saying, but this is not libraries that implement dynamic programming. There are general libraries for dynamic programing that are interesitng, see for example https://didp.ai/
72.
by mzl 1y ago
Would be interesting to see in next years MiniZinc challenge as a way to compare with other solvers.
73.
by mzl 1y ago
Looks interesting. Would it be possible to use it as a MiniZinc backend?
74.
by mzl 1y ago
The point of these types of systems is that you can store energy when it is cheap to do so (there is an abundance of wind and/or solar energy) and use it later.
75.
by mzl 1y ago
I've heard several talks about how some companies make AI systems that are designed to play as similar to human players as possible. This has been crucial for them in order to play-test levels in order to balance the game. And note, th
76.
Benchmarking MiniZinc and the LinkedIn Queens Problem(zayenz.se)
1 points by mzl 1y ago|0 comments
77.
by mzl 1y ago
> > they show that you can use SAT to solve Sudoku > Wait, did you mess up the direction here too, or am I confused? If you reduce problem A to B, then it means B is at least as hard as A, because solving it would solve A. Using S
78.
by mzl 1y ago
Adding to wavemode, the Sudoku example is a good starting point: https://github.com/Gecode/gecode/blob/master/examples/sudoku... In the documentation ( https://www.gecode.org/doc-late
79.
by mzl 1y ago
Note, the release/6.3.0 branch is the current release.
80.
by mzl 1y ago
LLMs can be run in a mostly deterministic mode (see https://docs.pytorch.org/docs/stable/notes/randomness.html for some info on running PyTorch programs). Varying the deployment type (chip model, number of ch
81.
by mzl 1y ago
That depends on the sampling strategy. Greedy sampling takes the max token at each step.
82.
by mzl 1y ago
Many compilers are not deterministic (it is why repeatable builds is not a solved problem), and many LLMs can be run in a mostly deterministic way.
83.
by mzl 1y ago
Yes, as a reviewer of a paper I am assigned a number, and must by nominative determinism fulfill the expectations...
84.
by mzl 1y ago
Thanks, luck of the draw ¯\_(ツ)_/¯ If you are interested in learning more about how to model problems with MiniZInc, there are several Coursera courses available: https://www.minizinc.org/resources/#courses-title
85.
by mzl 1y ago
I'd say, in general any time a time-value somehow originates as a part of an interaction with a human, that time-value carries with it the context of a timezone and the expectations of what that timezone means for that human. For inter
86.
by mzl 1y ago
As many others have said, time and calendars is messy, and there is often no correct solution but just a bunch of trade-offs. Jon Skeets Storing UTC is not a Silver Bullet ( https://codeblog.jonskeet.uk/2019/03/27&#
87.
by mzl 1y ago
Directly modelling the unique solution property would be a quantified problem, essentially it would be "there exists a solution such that it is not the case that there exists a different solution". In principle, you can explode th
88.
by mzl 1y ago
Generally what is needed is a subroutine that can tell you 1) if the problem has a solution, and 2) if the solution is unique (common requirement for puzzles like these). Using such a model as a sub-routine, a heuristic search can be done t
89.
by mzl 1y ago
You might be interested in looking at MiniZinc ( https://minizinc.org/ ) which is an open source modelling language for combinatorial problems. The system comes from a constraint programming background but the language is sol
90.
by mzl 1y ago
SAT (satisfiability), SMT (satisfiability modulo theories), CP (constraint programming) and so on are not magic solutions. They are more or less really smart backtracking solvers that use lots of heuristics, deductions based on the constrai

More ›