2) http://attractivechaos.wordpress.com/2011/06/19/an-incomplet...
That said, one thing that I always felt was unique about LP was how one of the primitive operations was data structure unification and how some pieces of code can be run in both "directions" if you are careful. However, I still haven't been able to find a neat example of what sort of problem really benefits from this.
I think one of the clear benefits is having a tool to aid you in your research. Speaking about chess, is like what Kasparov envisioned for advanced chess http://en.wikipedia.org/wiki/Advanced_Chess
For example, imagine that you want to implement a professional chess software. One romantic approach would be to find the best and nicest algorithm(s) to do that. SMT, idealistically, adds some "ugliness" trying to reach to a conclusion using every heuristic available. It's an algorithm too but it doesn't end on a good expressiveness but in inserting every heuristic available inside the resolution process.
Even programming languages like Prolog needs an expression of the problem that is not exactly how we think in logical expressions. You can't directly translate a first order logic expression to Prolog, you need to add extra thinking before doing that.
On the other hand generic combinatorics libraries don't work with large sets.
Welcome to SMT (satisfiability modulo theories) where there are state of the art optimizations for specific fields. If you want to see something impressive look at how to solve Sudoku with Z3 (http://z3.codeplex.com/) , it's just expressing the problem in logic terms: http://rise4fun.com/Z3Py/tutorialcontent/guide#h210