  We apply Boolean Satisfiability (SAT) and Satisfiability Modulo Theories
(SMT) solvers in the context of finding chiral heterotic string models with
positive cosmological constant from $\mathbb{Z}_2\times \mathbb{Z}_2$
orbifolds. The power of using SAT/SMT solvers to sift large parameter spaces
quickly to decide satisfiability, both to declare and prove unsatisfiability
and to declare satisfiability, are demonstrated in this setting. These models
are partly chosen to be small enough to plot the performance against exhaustive
search, which takes around 2 hours 20 minutes to comb through the parameter
space. We show that making use of SMT based techniques with integer encoding is
rather simple and effective, while a more careful Boolean SAT encoding provides
a significant speed-up -- determining satisfiability or unsatisfiability has,
in our experiments varied between 0.03 and 0.06 seconds, while determining all
models (where models exist) took 19 seconds for a constraint system that allows
for 2048 models and 8.4 seconds for a constraint system that admits 640 models.
We thus gain several orders of magnitude in speed, and this advantage is set to
grow with a growing parameter space. This holds the promise that the method
scales well beyond the initial problem we have used it for in this paper.
