Various approaches to solving set theory constraints exist, e.g., within verification tools for TLA+ or the B method. In this paper we present a way to solve set theory constraints in general and B formulas in particular using SAT solvers, by using Prolog technology. First, a preliminary analysis uses CLP(FD) constraint solving to infer finite bounds for all variables. Second, Prolog translation rules map constraints to answer set programming (ASP), by encoding logical and set-theoretic operators as Horn clauses. Finally, the Clingo tool is used to translate the ASP encoding to SAT, and the generated models are translated back to set theory and B using Prolog DCG rules. The scheme of the paper has been implemented in SICStus Prolog, as an alternate backend for the ProB validation tool, which we evaluate on a series of benchmarks. Our paper highlights the usefulness of Prolog, for analysis, inference and transformation rules and ASP as a high-level interface to SAT solving.