A new pseudo-Boolean satisfiability based approach to power mode schedulability analysis

It is important to know for a collection of tasks running in hand-held devices, if there is any way to schedule power modes to them which maintains every temporal and power constraints. The peak power that the battery in the system can deliver at any moment plays crucial role in deciding schedulability. We propose a pseudo-Boolean satisfiability (PB-SAT) based approach for solving this schedulability problem of power modes for a collection of tasks. We show that in majority of useful cases, the problem can be encoded using linear constraints only and thus becomes an instance of PB-SAT problem. We also show how we can find out a mode allocation using PB-SAT approach that ensures minimum power consumption, but never violates any temporal constraint. We also propose a binary search based approach with PB-SAT as its core, how we can find out the bare minimum value of the battery peak power that allows a power mode allocation to the tasks without violating its temporal constraints. Results show that the approach gives acceptable results in many cases