Posted: 1/17/2013 8:11 AM
Post subject: SAT solvers: let them find the best solutions for your game!
Quote
partyboy1a
Player (136)
Joined: 9/18/2007
Posts: 389
Sometimes, your task is to solve a certain kind of puzzle optimally. At the same time, there are a lot of different possible solutions for the puzzle, probably more than you could ever handle. And now you ought to find the very best of all sollutions... This is where SAT solvers can come in very handy. These can solve the boolean satisfiability problem very very fast (most of the time). You just give them the rules of the game in an appropriate format, and it will find ONE solution for you (if a solution exists). So if it's still a solvable problem, you just have to add some more rules to find a better solution. At some point, you will have found the best solution this way, AND you even proved that the solution is optimal. The biggest problem about that is: You have to translate the game into a set of just boolean variables. This is quite hard, you need to consider absolutely every detail, even the most "trivial" rules, and rules you wouldn't really think of. So it's limited to games where you really know ALL rules. However, I got it to work for DS Polarium (there it is relatively slow on small puzzles, but very fast for larger or more difficult ones), and I made a small SAT-solver-framework.lua which simplifies the task of entering clauses, and a sample file on how to use it... I used it to implement the rules of Tetris (well, only 1 / 20th right now, and I will most probably not implement the rest, I think there is already very good software available for this game...) in a way so that a SAT solver can understand it, get Tetris.lua here. Can you think of more games where such a SAT solver approach may work?
Posted: 1/22/2013 5:09 PM
Quote
GMan
Joined: 4/7/2008
Posts: 117
I've been investigating the use of automatic theorem provers for solving TASes lately, coincidentally. Don't want to to give out a bunch of information because people will inevitably get their hopes up for no reason, but I've been writing a new emulator as a hobby project where each system has a uniform simulation interface. This lets you perform symbolic execution on the system, and I'm trying to leverage constraint solvers (namely Z3) and automatic theorem proving to make conjectures about the game and prove them, ultimately conjectures of the form "this is the fastest way to satisfy these constraints: ...". (The "normal" approach of concolic testing isn't tractable for anything but small inputs.) I originally intended to try to automate TASing with genetic algorithms, but this intrusive apporach is much better, and can (in theory) give provably optimal solutions. The genetic algorithm approach was fun though, because half the task was leveraging existing emulators to be evaluation functions. But it was extremely difficult to produce good results without also introducing learning, so I reapproached it from a formal learning side. This is just a hobby project for now though. Good work on leveraging SAT!
Posted: 1/24/2013 10:15 PM
Quote
partyboy1a
Player (136)
Joined: 9/18/2007
Posts: 389
"genetic" algorithms? I think that is much too resource-intensive to be doable in the near and in the far future... Also It cannot be possible to find the "best" solutions without human interaction... The least what is required is to tell the program when you "win", and this alone is a difficult task, and may even be subjective (just think of the glitched version of Super Mario World, which shows "The End" while playing a normal level). Just defining the winning condition is most likely only possible by disassembling each game, every single line of code... However, I wish you good luck with your project!
Posted: 1/24/2013 11:45 PM
Quote
CoolKirby
Editor, Experienced player (608)
Joined: 11/8/2010
Posts: 4012
Exotic platforms TASer of 2014 NES TAS of 2013
partyboy1a wrote:
The least what is required is to tell the program when you "win", and this alone is a difficult task, and may even be subjective (just think of the glitched version of Super Mario World, which shows "The End" while playing a normal level).
Actually, in that run, it's not just a graphical change. The game is actually tricked into loading the The End sequence. (You can't press any button to continue the game when that screen appears, you can only restart the system in order to continue, just like when you reach that screen without manipulating memory.) So an algorithm like this actually could check for that end state, and would return a positive value if it checked that particular glitched run.
Posted: 1/25/2013 3:00 AM
Quote
GMan
Joined: 4/7/2008
Posts: 117
partyboy1a wrote:
"genetic" algorithms? I think that is much too resource-intensive to be doable in the near and in the far future...
Er, I don't see how. Perhaps you mean it'll take too long? I agree with that if we're using pure genetic algorithms on input, which is why I said you'd have to introduce learning for this to be feasible. But the genetic algorithms themselves aren't very resource intensive. Here's a video I uploaded a while ago but never made public (made public now): Link to video It's shows the result of an extremely basic genetic algorithm. The one on the left is the original input, the one on the right was the genetic result. This was quite fun to make because I ran Mupen64 in my process space so I could manipulate it by changing its variables programmatically (which itself was a fun process of finding their addresses). I think I had 8 or 32 Mupen instances running concurrently for that video. The way it works is that an input sequence is evaluated against some fitness function (in this case it was distance from honeycomb summed across all frames, ergo getting there fastest maximized fitness). The multiple Mupen instances allowed me to evaluated multiple sequences at once (this is just optimization, not necessary for correctness). The N most fit sequences in the population are chosen to survive, and "mate" by mixing their input sequences using genetic crossover with random mutations. Then this new population is tested and so on. Over (infinite) time, this maximizes fitness. Obviously we don't have infinite time, so it's up to practical concerns to decide when it's finished.
partyboy1a wrote:
Also: It cannot be possible to find the "best" solutions without human interaction... The least what is required is to tell the program when you "win", and this alone is a difficult task, and may even be subjective (just think of the glitched version of Super Mario World, which shows "The End" while playing a normal level). Just defining the winning condition is most likely only possible by disassembling each game, every single line of code...
Right, the automation is only for the task of satisfying a goal, the goal is still specified by external input (human). And yes, this does require you understand what values certain memory addresses take on, but this generally isn't too difficult to find out. And it only has to be figured out once. (For the example above I only needed to know the location of the honeycomb and the location of Banjo.) But like I said, the genetic algorithm just doesn't converge fast enough without learning, and if I'm going to do learning I'd rather take a more formal approach.
Posted: 1/29/2013 5:24 AM
Quote
Personman
Other
Joined: 4/20/2008
Posts: 465
This is delightful. Would very much appreciate any info/progress you feel like posting, even if nothing ever comes of it.
A warb degombs the brangy. Your gitch zanks and leils the warb.
Posted: 1/29/2013 2:11 PM
Quote
partyboy1a
Player (136)
Joined: 9/18/2007
Posts: 389
Another attempt for the SAT solver: Yoshis Cookies (+ SAT solver framework + minisat / picosat) Performance is quite bad. If the puzzle is just a little bit more complicated, then the solver can take forever...