text: Over the last decade , a variety of SMT algorithms have been built and empirically tested whereas little is known about the [[ computational complexity ]] of some of the fundamental << problems >> of SMT .