SAT is about a very special case of logic, namely propositional logic, where every variable stands for exactly one of only two possible truth values. Finding satisfying assignments in propositional logic is indeed already a computationally hard task, and it is good that we have efficient SAT solvers for such use cases, allowing us to solve a large variety of combinatorial problems nowadays.
However, Prolog lets you tackle not only propositional logic, but tasks that go far beyond this, belonging to a logic called classical first order logic, of which propositional logic is only a subset. In first order logic, we reason about predicates between terms, and this lets you tackle much more complex tasks, far beyond what SAT/SMT solvers can solve for you.
In fact, first order logic is so powerful that it lets you describe everything you can in principle perform with a computer. It lets you describe how a compiler works, for example. Or how numerical integration works. And all other computations you have ever seen computers perform.
In short, Prolog is a programming language, and can in fact even be used to implement a SAT solver, which is impossible to do with just a SAT solver. Many Prolog implementations even ship with a SAT solver as one of their libraries.
There are also even higher-order constructs in Prolog, such as predicates that let you invoke other predicates, making programming in Prolog very expressive and convenient.
> first order logic is so powerful that it lets you describe everything you can in principle perform with a computer
Not quite sure what you're referring to here, but induction schemata seem to be a notable exception. There's a reason higher-order logic is often preferred for software verification.
I guess FOL is adequate if you're allowed to have an infinite number of axioms, but that doesn't seem very satisfying (pun intended).
I am referring here to the fact that first-order logic is sufficiently expressive to describe how a Turing machine works, making FOL Turing-complete and thus, as a special case, making every computation you can carry out on a computer expressible in FOL, as a first-order formula that is satisfiable iff the TM accepts the input.
SMT solvers typically only support decidable theories, and since first-order logic is not decidable (only semi-decidable), such solvers are not as expressive as Prolog.
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.
This expresses Fermat's Last Theorem in terms of CLP(FD). A constraint solver with perfect propagation (which, as we know, cannot exist for the integers) would deduce that this conjunction of constraints cannot hold.
Answer-set programming (ASP) is another direction to go in w.r.t. this relationship. It takes a Prolog-like semantics (and syntax), but rebases the solving process on top of a solver-style backend that shares some general similarities with SMT/SAT-style propositional solvers. The semantics of ASP were initially arrived at as one of several attempts to give a conventional logical semantics to Prolog. Prolog's semantics from the perspective of traditional logic are a bit obscure, because it's defined in a somewhat imperative manner as "whatever SLDNF gives you", which includes things like statement order being significant (queries might terminate under one ordering and not under another, which is not something you find in logical semantics).
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).
