I think what you're saying is that you can take a Prolog program and ground it all down to the propositional order so you can then evaluate it with a SAT solver. For example, you can take a Prolog clause like this one:
p(X,Y):- q(X,Z), r(Z,Y)
And ground it in all possible ways with constants in the domain of discourse:
And so on, at which point you essentially have propositional formulae, like:
p1 :- q1, r1
p2 :- q2, r2
...
etc.
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.
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.