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"):
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)