SMT 솔버를 사용하여 JIRA 티켓 관리하기

2024년 2월 1일 · 태그: programming, python, formal · 원문 · 한국어 번역(원문에서 변경됨)

관리자가 정기적으로 마주치는 흔하고 종종 지루한 문제 중 하나는 작업 일정 계획입니다. 이는 특히 프로젝트 관리에서 중요한데, 다양한 제약 조건을 준수하면서 팀원에게 작업을 할당하는 일은 복잡한 과제가 될 수 있습니다. 제약에는 가용성, 기술 수준, 마감 기한, 워크로드 균형 등이 포함될 수 있습니다. 이러한 문제를 수작업으로 해결하면 오류가 발생하기 쉽고 시간도 많이 걸리지만, Microsoft Research에서 개발한 오픈 소스 SMT(Satisfiability Modulo Theories) 솔버인 Z3의 힘을 빌리면 이 과정을 효율적으로 자동화할 수 있습니다.

팀원에게 할당해야 하는 일련의 작업이 있는 프로젝트를 관리하고 있다고 상상해 보십시오. 각 작업에는 특정한 소요 시간이 있고, 각 팀원의 가용 시간은 제한되어 있습니다. 또한 일부 작업은 다른 작업이 완료될 때까지 시작할 수 없습니다. 여기서는 Z3가 어떻게 이 일정 계획 문제를 자동화하여 모든 제약 조건을 충족하고 작업을 최적으로 할당하도록 돕는지 살펴보겠습니다.

다음과 같은 실제 시나리오를 생각해 봅시다.

팀원은 Alice, Bob, Charlie 3명입니다.
작업은 5개이며, 각 작업에 필요한 시간은 서로 다릅니다.
각 팀원의 가용 시간(일할 수 있는 시간)은 제한되어 있습니다.
일부 작업에는 의존 관계가 있어 특정 순서대로 완료해야 합니다.

작업과 각 작업의 소요 시간(시간 단위)은 다음과 같습니다.

작업 1: 3시간
작업 2: 2시간
작업 3: 4시간
작업 4: 2시간
작업 5: 1시간

팀원의 가용 시간(시간 단위)은 다음과 같습니다.

Alice: 5시간
Bob: 4시간
Charlie: 3시간

의존 관계는 다음과 같습니다.

작업 3은 작업 1이 완료될 때까지 시작할 수 없습니다
작업 5는 작업 4가 완료될 때까지 시작할 수 없습니다

Z3를 사용하여 이 문제를 풀어 봅시다. 먼저 Z3 패키지를 설치해야 합니다.

pip install z3-solver

이제 문제를 푸는 코드를 작성해 봅시다.

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!")

이 코드는 문제와 제약 조건을 정의한 다음, Z3를 사용하여 팀원에게 작업을 유효하게 할당하는 방법을 찾습니다. task_assignment 딕셔너리는 각 작업에 할당된 팀원을 담고 있으며, solver.add 메서드는 솔버에 제약 조건을 추가하는 데 사용됩니다. 마지막으로 solver.check 메서드로 해를 확인하고, model을 사용하여 할당된 작업을 출력합니다.

Keyboard shortcuts

Stephen Diehl 블로그 한국어 번역

SMT 솔버를 사용하여 JIRA 티켓 관리하기