0
Z3을 사용하여 작업 상점 스케줄링 문제점을 모델링하려고합니다. 특히 각각의 작업에 다른 작업 종속성이있는 작업 집합이 있다고 가정 해 봅시다. 그런 다음 마지막 작업, 즉 메이 판을 예약하는 시간을 최소화하고 싶습니다.Z3을 사용하여 스케줄링 문제점을 최소화하십시오.
다른 작업에 종속되지만 앞으로 종속성이없는 작업이 여러 개있을 수 있으므로 (작업이이 작업에 종속되지 않음) Z3의 간단한 최소화 작업으로는 충분하지 않을 수 있습니다. 그리고 Z3은 목록에 대한 최대 기능을 인정하지 않습니다.
따라서이 문제를 해결하기 위해 모든 작업에 따라 위조 된 작업을 추가하고이 작업을 예약하는 시간을 최소화 할 것을 고려 중입니다. 나는 많은 작업에 제약 조건을 추가 할 필요가 있기 때문에이 접근법이 확장 성이 있는지 궁금합니다.
이 방법이 유일한 방법입니까 아니면 다른 더 효과적인 방법입니까?
해결하려는 문제의 구체적인 예를 추가 할 수 있습니까? 특히 쿼리 시간에 알려진 작업 수는 얼마입니까? –