An SMT Approach To A Multiparty Economic Scheduling Problem

Palakodety, Shriphani and Jayachandran, Guha and Thakur, Aditya V.
17th International Workshop on Satisfiability Modulo Theories (SMT’19), 2019

We discuss a multiparty resource allocation problem in a digital marketplace for purchase and sale of compute resources. The problem exhibits several challenging characteristics: (i) multiple agents and resources in a single matching instance, (ii) constraints that can be imposed on individual resources or a combination of resources, and (iii) short wall clock time for production settings. We model the problem as a satisfiability problem, and discuss an implementation using the Z3 SMT solver.

PDF    

@inproceedings{SMT2019,
  author = {Palakodety, Shriphani and Jayachandran, Guha and Thakur, Aditya V.},
  title = {An SMT Approach To A Multiparty Economic Scheduling Problem},
  booktitle = {17th International Workshop on Satisfiability Modulo Theories (SMT'19)},
  year = {2019}
}