I think Prologs big strength amongst others is the meta interpreter and higher order functions which I think are essentially tied to SLD.
Prolog has predicates, not functions. (It has uninterpreted function symbols -- aka functors in this context.) It's based on first-order logic, i.e., it has nothing higher order in it, if you want to take it (formally) seriously. But of course there is `call/1` and so forth, which are just hacks... err, "non declarative".
There are some interesting higher-order logic programming languages, e.g. Mercury. I like the approach taken by HiLog [1] as it struck me as (semantically) honest and simple. I don't know if it's usable.
To clarify. A FOL language begins with an "alphabet" (sometimes called a "signature") of predicate symbols, function symbols (including constants), variables, the five logical connectives (¬, ∧, ∨, →, and ↔) and punctuation (left and right parens, comma, dot, colon). The sets of predicate, function and variable symbols are disjoint.
Function symbols are used to define terms, inductively, as follows. A variable is a term; a constant is a term; if f is a function symbol and t_1, ..., t_n are terms, then f(t_1, ..., t_n) is a term.
Terms are used to define formulae as follows: If P is a predicate symbol and t_1, ..., t_n are terms, then P(t_1, ..., t_n) is an atomic formula, or atom. If φ is a formula, then ¬φ is a formula. If φ, ψ are formulae, then φ ∧ ψ, φ ∨ ψ, φ → ψ, and φ ↔ ψ are formulae.
Literals and clauses are defined as follows: if A is an atom, then A is a positive literal and ¬A is a negative literal. A clause is a disjunction of literals. A clause with a single positive literal is definite. A definite clause with no function symbols other than constants is datalog.
Now, if you squint a bit at all of the above and then at a Prolog program you will see a serious violation of the rules of FOL syntax. Observe:
This is Prolog:
p(x, y):- q(r(x),z), r(p(x,z)).
But Prolog doesn't care. Prolog doesn't care if an object is a predicate, or a function, if it's a mapping, or a relation. For Prolog there's no distinction, and because there's no distinction it can treat everything as an argument to everything else: an atomic formula can be "passed" to an atomic formula, and taken apart, and put back together again. For example, you can do this sort of thing:
?- T_ =.. [p,X,Y,Z], T =.. [r,T_].
T_ = p(X, Y, Z),
T = r(p(X, Y, Z)).
prove(L):- true.
prove(L,Ls):- prove(L), prove(Ls).
prove(L):- L \= (_,_), clause(L,Bs), prove(Bs).
Btw, I'm not at all complaining about Prolog's higher-order. That may be a "hidden" feature, but it's a really, really useful one. FOL is actually very restrictive in many ways. As far as I understand it, the distinction between first and higher-order logics was not made by Peirce and Frege, who tended to fudge the orders a lot, just like Prolog.
In any case, for me, logic programming begins and ends with Robinson's paper on Resolution. That was not about formal semantics, and only about a sound and complete inference rule. And that (soundness and completeness) is all I really need to know. The rest (including definite clauses, SLD-Resolution and Prolog) is all implementation details.
To clarify, datalog is a restriction of Prolog excluding functions of more than 0 arguments (i.e. constants). For example, P(x,y) :- Q(f(x), g(y)) is Prolog but not datalog. There's also a restriction in the sharing of variables between head and body literals that ensures termination. The point of datalog is that because of its function-free structure it's decidable. You could simply ground a datalog program and get its entire Herbrand model.
SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint solving. I don't know why it (or SAT) is compared to Prolog which has nothing to do with boolean satisfiability problems.
ASP also has nothing much to do with Prolog. It's a strictly first-order language (Prolog is higher-order) that is based on the idea of stable model semantics. Very briefly, a stable model is often the set of queries to which Prolog will answer "true" (or "yes" depending on the interpreter). ASP programs share some syntax with Prolog, but are not definite programs. For one thing, ASP allows classical negation, alongside Prolog's Negation-As-Failure. ASP is said to be well-suited to optimisation problems but to me it's more interesting as a formal treatment of reasoning under uncertainty in a strictly logic framework.
Note that datalog is incomplete (obviously, since it doesn't have functions) and ASP solvers are NP-complete. They are also special-purpose languages, so for example nobody is going to write a web server in ASP anytime soon. By comparison, the SWI-Prolog website runs on a web server written in Prolog (https://eu.swi-prolog.org/dogfood.html).
SMT and SAT are certainly less expressive than Prolog (or more abstract systems, like LambdaProlog, Isabelle/HOL, etc.), so they cannot express the same structures/abstractions. However, given any "concrete" query/program, we can collapse all of its structure, in-line/unroll all of its higher-order parts, etc. to get a SAT formula (modulo the halting problem).
The resulting term is usually exponentially-larger than the original; but SAT solvers have become fast enough to handle such giant problems. (SMT solvers are usually wrappers around a SAT solver too)
p(X,Y):- q(X,Z), r(Z,Y)
p(a,b):- q(a,c), r(c,b)
p(1,3):- q(1,2), r(2,3)
...
p1 :- q1, r1
p2 :- q2, r2
...
That's what ASP does (except it's not Prolog). But one problem with that is that it doesn't work in a language with functions, because then you get infinite groundings. So for example, ASP doesn't have lists (because you get infinite lists). Prolog does, and you can't just ground any old Prolog program, just like that.
Then again, the motivation behind Prolog's unification is exactly that you don't need to ground the entire Herbrand base of a Prolog program to evaluate it. You can unify variables, until you finally have only ground terms when the proof is complete, but no sooner than that. And of course, you can get a proof before you have only ground terms. So it's really not like SAT solving in my mind (given the very little I understand about SAT solving).
If I understand correctly, the Davis-Putnam algorithm used in SAT solving is based on Resolution in the propositional order, and Prolog is SLD-Resolution, that is a restriction of Resolution to definite clauses which are first-order (though Prolog is not first-order but higher-order as I say in another comment). So that's some common structure, there, but still, they're very different things.
sure, that's all true and most of that is part of my day-to-day research. But the post I replied to mentioned very specific problems where Prolog could be suitable at first glance but other models of computation / problem statement are usually preferred.
But most of those do have implementations that use Prolog-like syntax.
But again and again one uses extralogical constructs in Prolog programming.
Case in point: basically all your mentioned alternatives (Datalog, SMT, I'd add ASP) have implementations that use the Prolog syntax or something close to it with very similar semantics. But not being tied to that specific execution model can give you (better) answers or more complete answers, termination guarantees, or other things we might need.