Task Scheduling with Nonlinear Costs using SMT Solvers

There are many natural and engineering processes which require scheduling under nonlinear cost functions. Current tools and theories only support scheduling under linear cost functions. In this paper, we model the scheduling problem under nonlinear costs using Priced Timed Automata (PTA). We also present a translation from PTA to Satisfiability Modulo Theory (SMT) formulas whose models correspond to schedules which satisfy the scheduling constraints under a given cost bound. We present a case-study for batch scheduling in bio-manufacturing. We compare our results with UPPAAL CORA when the costs are linear. We show that the SMT based solution outperforms the UPPAAL CORA solver when the length of the schedule is bounded.