Which SAT solver should I tell Alloy to use?

The choice of SAT solver can be set in the Alloy Analyzer’s preference panel. For most analyses, the choice of the SAT solver doesn’t matter. MiniSat and ZChaff are good choices for small problems; for larger problems, Berkmin seems to perform best.