"Z3 integrates a modern DPLL-based SAT solver, a core theory solver that handles equalities and uninterpreted functions, satellite solvers (for arithmetic, arrays, etc.), and an E-matching abstract machine (for quantifiers)"

From http://research.microsoft.com/en-us/um/redmond/projects/z3/z...

I'm not well-versed on this topic, but I believe this [1] is presently the state of the art. I'd be curious to know whether or not Z3 performance beats GNU's prolog implementation for similar problem sets.

1: http://www.gprolog.org/#TOChead

I'm not sure which one exactly, but it's a SAT solver, so it uses a SAT solving algorithm [1].

1 - http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#...