Title
Task Scheduling with Nonlinear Costs using SMT Solvers
Abstract
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.
Year
DOI
Venue
2019
10.1109/COASE.2019.8843048
2019 IEEE 15th International Conference on Automation Science and Engineering (CASE)
Keywords
Field
DocType
task scheduling,SMT solvers,nonlinear cost functions,linear cost functions,PTA,batch scheduling,SMT based solution,priced timed automata,satisfiability modulo theory,biomanufacturing
Mathematical optimization,Job shop scheduling,Modulo,Scheduling (computing),Computer science,Satisfiability,Automaton,Schedule,Job scheduler,Solver
Conference
ISSN
ISBN
Citations 
2161-8070
978-1-7281-0357-0
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Mohammad Hekmatnejad111.05
Giulia Pedrielli21215.42
Georgios E. Fainekos380452.65
Mohammad Helunatnejad400.34