The main SAT solver monad. Embeds ST. See type SSTErrMonad, which stands
for ''State ST Error Monad''.
Most of the work done is in the form of SSTErrMonad actions.
SSTErrMonad e st s a: the error type e, state type st, ST thread
s and result type a.
This is a monad embedding ST and supporting error handling and state
threading. It uses CPS to avoid checking Left and Right for every
>>=; instead only checks on catchError. Idea adapted from