Time-Triggered Network-on-Chip (TTNoC) is a networking concept aiming at providing both predictable and high throughput communication for modern multiprocessor systems. The message scheduling is one of the major design challenges in TTNoC-based systems. The designers not only need to allocate time slots but also have to assign communication routes for all messages. This paper tackles the TTNoC scheduling problem and presents an approach based on Satisfiability Modulo Theories (SMT) solving. The authors first formulate the complete problem as an SMT instance, which can always compute a feasible solution if exists.