Using SMT Solvers to Manage JIRA Tickets

One common and often tedious problem that managers regularly encounter is task scheduling. This is particularly relevant in project management, where assigning tasks to team members in a manner that adheres to various constraints can become a complex challenge. Constraints can include availability, skill levels, deadlines, and workload balance. Solving such problems manually can be error-prone and time-consuming, but with the power of Z3, an open-source SMT (Satisfiability Modulo Theories) solver from Microsoft Research, we can automate this process efficiently.

Imagine you are managing a project with a set of tasks that need to be assigned to team members. Each task has a specific time requirement, and each team member has limited availability. Additionally, some tasks cannot be started until others are completed. Here, we’ll see how Z3 can help automate this scheduling problem, ensuring all constraints are met and tasks are assigned optimally.

Let's consider a real-world scenario where:

1. We have 3 team members: Alice, Bob, and Charlie.
2. There are 5 tasks, each requiring a different amount of time.
3. Each team member has limited availability (number of hours they can work).
4. Some tasks have dependencies and must be completed in a certain order.

The tasks and their durations (in hours) are as follows:

• Task 1: 3 hours
• Task 2: 2 hours
• Task 3: 4 hours
• Task 4: 2 hours
• Task 5: 1 hour

The availability of team members (in hours) is as follows:

• Alice: 5 hours
• Bob: 4 hours
• Charlie: 3 hours

The dependencies are:

• Task 3 cannot start until Task 1 is completed
• Task 5 cannot start until Task 4 is completed

Let's solve this problem using Z3. First, we need to install the Z3 package:

pip install z3-solver

Now, let's write the code to solve the problem:

from z3 import Int, Solver, And, If

# Create solver instance
solver = Solver()

# Define team members
team_members = ['Alice', 'Bob', 'Charlie']

# Define tasks and durations
tasks = {
    'Task 1': 3,
    'Task 2': 2,
    'Task 3': 4,
    'Task 4': 2,
    'Task 5': 1
}

# Define team member availability
availability = {
    'Alice': 5,
    'Bob': 4,
    'Charlie': 3
}

# Define task dependencies
dependencies = {
    'Task 3': ['Task 1'],
    'Task 5': ['Task 4']
}

# Create a dictionary to hold the assigned team member for each task
task_assignment = {task: Int(task.replace(' ', '_')) for task in tasks}

# Add constraints for team member availability
for member in team_members:
    solver.add(Sum([If(task_assignment[task] == i, tasks[task], 0) for task, i in zip(tasks, range(len(team_members)))]) <= availability[member])

# Add constraints for task dependencies
for task, deps in dependencies.items():
    for dep in deps:
        solver.add(task_assignment[task] > task_assignment[dep])

# Ensure each task is assigned to exactly one team member
for task in tasks:
    solver.add(And([task_assignment[task] == i for i in range(len(team_members))]))

# Check for solution
if solver.check() == sat:
    model = solver.model()
    for task in tasks:
        assigned_member_index = model[task_assignment[task]].as_long()
        print(f"{task} is assigned to {team_members[assigned_member_index]}")
else:
    print("No solution found!")

This code defines the problem and constraints, and then uses Z3 to find a valid assignment of tasks to team members. The task_assignment dictionary holds the assigned team member for each task, and the solver.add method is used to add the constraints to the solver. Finally, the solver.check method is used to check for a solution, and the model is used to print the assigned tasks.