What about SMT vs. Prolog, do Prolog have more expressiveness?
In Prolog, the more natural approach that closely corresponds to SMT is simply implementing the theory as a constraint solver. For example, check out CLP(FD) and CLP(Q) for constraint solvers over integers and rational numbers, respectively. They let you formulate statements over these theories, and search for solutions. Note though that solving equations over the second-order theory Z (i.e., integers) is not decidable either (only semi-decidable), and so you may search indefinitely if there is no solution.
Importantly, constraints over these theories blend in completely seamlessly into Prolog, since they are simply available as predicates. For example, we can write:
?- A^N + B^N #= C^N,
N #> 2,
[A,B,C] ins 1..sup.
ASP is based on one of those Prolog-semantic proposals, the "stable-model semantics", which competed with other proposals like the "well-founded semantics". Although these are first-order in principle, existing practical tools only implement propositional solvers. ASP systems still take a Prolog-like input language that looks first-order, but they work by first "grounding" the first-order formulae to a propositional representation, and then solving them. If you make suitable assumptions about finite domains etc. this has the same expressivity, but sometimes causes blow-up (other times it causes surprisingly fast-running programs, though).
This is a good open-source ASP system: https://potassco.org/