Those are games, not practical problems. I find SAT solvers exciting, but at the same time I’m so disappointed by how few problems they solve. So far it seems to be dependency management and key cutting.
Generally speaking, if you ever find yourself coding a brute-force backtracking search for some combinatorical problem, it might be a good idea to consider using a SAT solver instead. This way you get to take advantage of the non-chronological backtracking, and all the other tricks the SAT solvers implement.
I wrote the hexiom solver that got linked above and the motivation in that case was that I saw that someone tried to solve the puzzle with a hand-written backtracking search, but that their algorithm wasn't able to find a solution to one of the levels.
My version of the SAT solver managed to quickly find a solution for every case, including the highly symmetric one where the usual search algorithm got stuck. The nicest thing is that the implementation was very declarative, in that my job was to produce a set of constraints for the SAT solver, instead of to produce an imperative algorithm. The symmetry breaking was one example of something hat was very easy to do in a SAT-solver setting but which would be trickier to do by hand.
I found two remotely exploitable 0days in the Erlang VM with the use of a SAT solver.
They can trivially break lots of hash algorithms. You can also find bitwise equivalents to functions which you wouldn't naturally expect to be easily definable in terms of bitwise operations. You can extend existing concepts with a lot of extraordinary new functionality.
DO you have a quick explanation or any reference on using SAT solver to find equivalent bit-wise functions? I can see how you could easily verify equivalence, but I am struggling to see how you could use SAT solver to generate alternate functions using bit-wise operators.
When considering a small number of possible operations, I've found the optimum way to work this is to simply enumerate all binary expression trees of increasing length and determine if some valid assignment exists for any of them.
The beautiful thing about this line of research is that if you have a problem that can be reduced to key cutting, you're set. Particularly if you can learn the lock-charts (or whatever the data looks like in your higher-level problem domain) from data.
The magic sauce is in being able to combine these things. Chuck a bag full of keys, sans known tumblers (those are embedded in doors, you don't steal doors) into a machine and learn with eg. stochastic gradient descent what are tumblerset-candidates that satisfy the entire system. Sensor arrays + AI that thinks + machine learning = wow.
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
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.
Hexiom: https://github.com/hugomg/hexiom