Unrolling closures into SAT boolean formula
It's important to remember that SAT can only encode problems that are in $NP$, unless you use more than polynomial-length formulas. I'm not 100% sure, but I'm doubting your problem is in $NP$.

Consider the following function:

$F = \lambda x\ y \ldotp x x (\lambda y . y y)$

Now consider evaluating $F F (\lambda z \ldotp z)$.

This clearly runs forever, but we can also see that the argument given as $y$ will grow exponentially with the number of $\beta$ reductions you do.

Now, some things that aren't clear from the question:


  non-deterministically represented candidate program


What does this mean? Is the program non-deterministic? Or its representation? What even is a non-deterministic representation?


  static once created and have a small number of predefined variables within each combinator


Again, what does this mean? My example doesn't seem to fit this, but if whatever you're dealing with us Turing Complete, my gut says your problem is likely to be $EXPTIME$-hard.