Z3 is a satisfiability modulo theories (SMT) solver created by Microsoft Research under the MIT license. An SMT problem is a decision problem for first-order logical formulas with respect to combinations of background theories such as arithmetic, bit-vectors, arrays, and uninterpreted functions [1].

The RAIR Lab is focused on utilizing the Z3 framework for an applicable real-world implementation under the project name Z3TRO (Z3 Transit Route Observer). Suppose that a person is located in a high-density metropolitan area with a public transport system and is tasked with reaching a destination before a given time. Given all of the possible paths and methods of transportation that are readily available, is it possible to find an efficient path for that person to take to reach their destination within the given time constraint? Inspired by the strategic board game Scotland Yard, the RAIR Lab is developing Z3TRO to utilize Microsoft’s Z3 to find a satisfiable solution to the above scenario for any given metropolitan city.