Control Design of Autonomous Cars Using Satisfiability Modulo Theory

Autonomous cars are currently at the forefront of technological development. These vehicles can navigate independently, enabling them to move without human intervention. Given this capability, autonomous cars require a controlled design to navigate their intended destinations without deviating from their designated paths. This research aims to design a controller for autonomous cars to operate within predefined constraints and scenarios. This research proposes a formal control design based on Satisfiability Modulo Theory. The objective of this control design is to guarantee that the car's motion, particularly lateral movement, remains on the designated path, considering various scenarios such as road width, speed, vehicle length, front-wheel angle, and vehicle turning angle constraints. Simulations in this research encompass three road variations: flat, inclined, and curved roads from all cardinal directions. Furthermore, initial car angles are varied across four quadrants to determine the vehicle's ability to perform U-turns or change direction. The simulation results reveal that the obtained control design solution exhibits characteristics that ensure the autonomous car can operate following the defined constraints and scenarios. This performance is contingent on the type of road, the car's body angle, and the initial and final conditions of the autonomous car.