   Do you use existing decision procedures in your projects.
  I was discussing earlier with somebody AI in games, and mentioned to someone that I am a fan of using existing solvers in my projects for certain things.  The example that I used was the Minisat SAT solver and the Minisat+ pseudo-boolean solver.  Well, apparently the person who I was discussing this with thought it was very strange, so I was wondering if any of the rest of you use existing solvers in your work.I used Minisat to find minimal cost strategies in a recent RTS I was tinkering with when the problems didn't map elegantly to A*.  Personally, I found it to be a very easy tool to work with, and it is ridiculously fast.  I used A* for pathfinding and such, but for large scale strategies, I found Minisat+ to be far more efficient.  Previously I also used Yices for some strategy computation as well for stuff that didn't map well to the more traditional search stuff.So, do you use any pre-packaged solvers?  Even pre-packaged A* solutions?  How about non-A*, non-search stuff?   
  I must admit I am blissfully unaware of what packages might be out there. I write my own A* because that's pretty trivial, but would be interested in seeing what else is available and for which problem domains within games.   ;  Well, A* obviously relies on the capacity to judge a solution's quality as a sum of the quality of it's partial solutions [with some sort of heuristic to place bounds on the sum of the quality of missing terms].  For problems that do not exhibit this, or rather cannot be mapped in this sort of hill-climbing-with-backtracking representation, A* degrades into a regular search problem.  For problems whose solutions' value cannot be judged by the value of partial solutions, something like Minisat or some other general purpose reasoning engine becomes rather interesting.One of the things I've used it for, just to make a case for it's value, is to calculate strategic formations for the AI.  I poll my map to assign attributes to potential positions of interest, and describe the effects of choosing a given location for a given unit on other units in other areas.  I then ask the solver to place my units given some sort of expected threat, so as to maximize for some goal [defensive quality, survivability, damage done to attackers/defenders, etc].Since these units represent synergistic relationships to each other [two units can provide cover for each other], an A* representation [at least as I've used it] tends to explore cases of higher individual quality first, and system-wide quality later [which may be composed of partial solutions with poor individual quality, relying on this synergy for system wide quality].  The result is that the A* approach explores nearly all of the state space, because I cannot represent a good heuristic for this synergy for units that have not been placed.It finds an optimal solution, but slowly.  The solver on the other hand can grind through these rules rather easily, since I can describe to it relationships between units, rather than the effects of chosen units.  It approaches the problem in almost the reverse way as to how the A* approach does it.  The A* approach places units, and measures quality.  The solver looks at relationships, and infers unit placement from desirable relationships.It's entirely possible that a more clever person than myself would map this better to something like A* than I have in a way that would beat the solver.  Honestly though, I would still find it interesting, because the process of describing my AI to the solver consists of only about 15 lines of code, and is thus also pretty easy to debug.Anyway, the thread seems to not get much attention, so perhaps I'll let it sink into the abyss after this post.   ;  I have nothing to add to the discussion, but this is the most interesting anecdote of AI implementation I've read (never even heard of satisfiability), so I don't reckon the topic needs to sink. Consider me intrigued. How easy was it to integrate Minisat? Is it possible to post a quick example of the system's determination?   ;  I don't see why you would think of using A* for this optimization problem: It doesn't sound like something that can naturally be thought of as a shortest-path problem. Not that I understand how you converted an optimization process into a SAT problem either...My first instinct for a problem like this would be to first try something simple: Loop through the units, placing each one where the objective function is maximized; do the loop several times hoping that the process converges, or at least that it leaves you with an acceptable configuration. If that is not good enough, I would try playing with simulated annealing.Of course I am assuming that the search space is too vast for an exhaustive search to be practical.EDIT: The only kind of pre-packaged solver that I've seen people use often is a Linear Programming solver. I find that mapping a problem to the Linear Programming paradigm is sometimes very limiting or forces twisted ways of thinking. In my limited experience, problems with Linear Programming solvers are hard to debug, so I am not a big fan.