The question is perfectly well-formed! It is, however, very broad, and I try to answer it very broadly. First, SAT solvers are powerful and efficient. SAT is

The question is perfectly well-formed! It is, however, very broad, and I try to answer it very broadly. First, SAT solvers are powerful and efficient. SAT is one of the most studied problems in CS, both from a theoretical and practical perspective. Donald Knuth dedicates a huge portion of The Art of Computer Programming to exactly this topic. For example, quoting from https://www-cs-faculty.stanford.edu/~knuth/news.html https://www-cs-faculty.stanford.edu/~knuth/news.html: Satisfiability is far from an abstract exercise in understanding formal systems. Revolutionary methods for solving such problems emerged at the beginning of the twenty-first century, and they've led to game-changing applications in industry. These so-called “SAT solvers” can now routinely find solutions to practical problems that involve millions of variables and were thought until very recently to be hopelessly difficult. I highly recommend this as a profound treatment of the subject for readers at all levels of expertise. Second, SAT solvers can be combined seamlessly with Prolog. In Prolog terminology, SAT is CLP(B), constraint logic programming over Boolean variables. From the perspective of a Prolog application programmer, you simply state what must hold about the variables, using Prolog predicates like conjunction, disjunction etc., you state which variables must be 1 and which must be 0 etc. Internally, a Prolog system may invoke an external SAT solver, or implement its own version of SAT solving, to find a satisfying assignment. Both approaches exist in the literature and in practice. For example, see A Pearl on SAT Solving in Prolog by Jacob M. Howe and Andy King: http://www.staff.city.ac.uk/~jacob/solver/ http://www.staff.city.ac.uk/~jacob/solver/ As another approach and reference, I have put together a small page about a different CLP(B) system that internally uses Binary Decision Diagrams (BDDs) to solve SAT instances: https://www.metalevel.at/clpb/ https://www.metalevel.at/clpb/ Third and finally, SAT is a comparatively low-level approach for expressing combinatorial tasks. Perfectly doable (for example, by automatic translation/compilation to SAT), but still low-level. That does not mean that it's inadequate. In fact, some aspects of the "true structure" of a problem may reveal themselves and allow an efficient solution only at that low level. It is perfectly possible to express Sudoku as a SAT problem, using CLP(B). For example: sudoku(Rows) :- length(Rows, 9), maplist(same_length(Rows), Rows), maplist(row_booleans, Rows, BRows), maplist(booleans_distinct, BRows), transpose(BRows, BColumns), maplist(booleans_distinct, BColumns), BRows = [As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is], blocks(As, Bs, Cs), blocks(Ds, Es, Fs), blocks(Gs, Hs, Is). blocks([], [], []). blocks([N1,N2,N3|Ns1], [N4,N5,N6|Ns2], [N7,N8,N9|Ns3]) :- booleans_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]), blocks(Ns1, Ns2, Ns3). booleans_distinct(Bs) :- transpose(Bs, Ts), maplist(card1, Ts). card1(Bs) :- sat(card([1],Bs)). row_booleans(Row, Bs) :- same_length(Row, Bs), maplist(cell_boolean, Row, Bs). cell_boolean(Num, Bs) :- length(Bs, 9), sat(card([1],Bs)), element(Num, Bs, 1). But the general point remains: Working - for example - with integers or Herbrand terms, or rational numbers etc., is more high-level and a more natural fit for many combinatorial tasks of practical relevance, and often allows also more efficient and more complete propagation, because more of the high-level structure of a task can be taken into account.