Skip to main content

Resource allocation using an SMT solver.

Project description


A collection of utility functions for using Microsoft's Z3 theorem prover to find the maximal allocation of limited resources given a prioritized list of discrete tasks to be executed.

Resources and Tasks

smartalloc is designed to be as thin of a wrapper around the Z3 library as possible, so it does not define classes called "Resource" or "Task."

Instead, Z3 primitives, such as Int or Real, are considered the resources, and tasks that they are allocated for are represented by (collections of) Z3 constraints.


The main workhorse of smartalloc is the allocate() function. It takes two arguments: the intrinsic constraints on the resources, and a list of the constraints required for each task.

Intrinsic resource constraints are applied immediately, and if the system already has no solution then an exception will be raised. After this, the constraints for each task are added to the system. If the system is still satisfiable then the task is considered "worked" and the next task will be added. If the system is not satisfiable, that task will be removed from the system before moving to the next. All tasks provided will be attempted to be added to the system; the ordering of the tasks determines which tasks get to claim their necessary resources first.

The allocate() function returns a tuple of two items. The first is the allocation description object (in the form of a Z3 model). The value of a resource variable can be retrieved from it by using it like a dictionary with the resource variable as the key. The second is a list of the indices of the tasks from the input are "worked" in the allocation result.

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

smartalloc-0.0.1.tar.gz (4.1 kB view hashes)

Uploaded source

Built Distribution

smartalloc-0.0.1-py2.py3-none-any.whl (4.6 kB view hashes)

Uploaded py2 py3

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Huawei Huawei PSF Sponsor Microsoft Microsoft PSF Sponsor NVIDIA NVIDIA PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page