It scales to much bigger problems, that's the impressive part. You can solve a small SAT problem with simple backtracking search, but try to solve a problem wit

It scales to much bigger problems, that's the impressive part. You can solve a small SAT problem with simple backtracking search, but try to solve a problem with millions of variables and tens of millions of constraints and suddenly your backtracking search is laughably slow. This is like that but at a higher level of expressivity. Having both classical negation and negation as failure allows for easy modelling of uncertainty for example. We don't know if P=NP but with how efficient these tools are in practice, maybe it doesn't matter that much x)