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
In case anyone is looking for other novel ways to solve Sudoku. I wrote a CP language a while back that does pretty fast solving for the right kind of problem [1]. Folks might also find this Sudoku benchmarking blog post interesting [2], it includes links to solutions in a bunch of languages.
The SMT bit you mentioned shines a light in one of the gripes I have with logic programming: most often the examples people give are for the sort of AI search problem that might look nice when specified but that you can't hope to solve in practice with a generic depth-first-search.
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.
At UBS I know they have a small business rules system written in core.logic, in their case I believe being able to run backwards allows them to uncover redundancies - like "which rules match this result".
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
I think this is also missing the point a bit. SMT solvers are great, but as far I can it's not really SMT vs. CP or LP, they have different strengths and weaknesses. As far as the sudoku example while neat is pretty much identical in approach and expressiveness to the core.logic version I linked to.
It's true that they are similar on their expressiveness approach and at the end core.logic could have an SMT making them identical. But when we add SMT we are talking about a different beast.
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