Solving Temporal Problems Using SMT: Weak Controllability