Submitted: February 2018
Abstract
This thesis addresses the translation of the GomX-3 battery-aware scheduling problem into a Satisfiability Modulo Theories problem, extended by the capability of finding optimal assignments according to a certain objective. GomX-3 was a low-earth-orbiting CubeSat by Danish satellite manufacturer GomSpace with a mission time of one year. A previous approach modeled the problem as network of linear priced timed automata, using cost-optimal reachability analysis on the network to produce a schedule. We discuss the Optimization Modulo Theories (OMT) formalization process of the problem set in terms of ease of modeling, flexibility and extendability as well as the computational efficiency of corresponding tools compared to the previous approach. The resulting tool synthesizes a time-discrete OMT program given lists of operational windows and the scheduling horizon of interest and uses the OMT solver OptiMathSAT to solve it. We then discuss how this approach fares against existing ones in terms of schedule quality and computational complexity on a set of benchmarks. We observe a great fit between scheduling problems and OMT based solutions.