News for hackers. Stuff that matters.

A comment on Modern SAT solvers: fast, neat and underused. Parent comment

Re:Modern SAT solvers: fast, neat and underused by __s on Sunday May 19, 2019 @11:58AM (#19953918)
Why fund DeepMind? Blink stalker micro & beating some old board game can't possibly be useful. Yes, we should also ignore Game Theory because it's just games, nothing practical

The complaint was having to compile problems into boolean satisifiability problems. Here we see one need only describe their problems as puzzles. These examples are nice in that they include code that shows how straight forward description of these problems can be

[ Parent | on HN ]
Re:Modern SAT solvers: fast, neat and underused by travisjungroth on Sunday May 19, 2019 @05:42PM (#19955700)
I called those out as not practical problems because the commenter specifically asked for that. I’m all for research, but there’s this bait and switch that goes on with SMT solvers. They’re presented as useful (TFA says “underused”) and when someone asks for real life use cases, people show minesweeper.
[ Parent | on HN ]