Task scheduling with nonlinear costs using SMT solvers

Mohammad Hekmatnejad, Giulia Pedrielli, Georgios Fainekos

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication2019 IEEE 15th International Conference on Automation Science and Engineering, CASE 2019
PublisherIEEE Computer Society
Pages183-188
Number of pages6
ISBN (Electronic)9781728103556
DOIs
StatePublished - Aug 2019
Event15th IEEE International Conference on Automation Science and Engineering, CASE 2019 - Vancouver, Canada
Duration: Aug 22 2019Aug 26 2019

Publication series

NameIEEE International Conference on Automation Science and Engineering
Volume2019-August
ISSN (Print)2161-8070
ISSN (Electronic)2161-8089

Conference

Conference15th IEEE International Conference on Automation Science and Engineering, CASE 2019
CountryCanada
CityVancouver
Period8/22/198/26/19

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Task scheduling with nonlinear costs using SMT solvers'. Together they form a unique fingerprint.

Cite this