Automating Elevator Design with Satisfiability Modulo Theories

Automating the design of elevator systems poses interesting challenges when it comes to deal with configuration constraints and to express "quality-of-design" targets that must also comply to specific norms and regulations. Our automated elevator design tool LIFTCREATE is based on an AI engine featuring special-purpose heuristic techniques which are successful in handling complex real-world designs, but are lacking flexibility and thus are difficult to extend to, e.g., different classes of systems or different norms and regulations. In this paper we describe the development of a replacement engine for L IFTCREATE which seeks to overcome the limitations of the current one. The new approach is based on satisfiability modulo theories (SMT) with theories of cost. We describe encodings to solve choice and placement of critical components in the elevator, and we experiment with our encodings using a state-of-the-art SMT solver. Our experiments show that the SMT-based approach is competitive with respect to the heuristic-based one, both in terms of efficiency and in terms of design quality.