Изменения
Нет описания правки
==Доказательство корректности==
{{Утверждение |about=#1
|statement= В расписании с обычными дедлайнами нет опозданий тогда и только тогда, когда нет опозданий в расписании с
вынужденными дедлайнами.
}}
{{Утверждение |about=#2
|statement= Если существует расписание без опоздание, то приведенный выше алгоритм найдет такое расписание.
|proof= Пусть <tex>x(1), x(2),...,x(n)</tex> {{---}} расписание, построенное этим алгоритмом, где <tex>x(i)</tex> {{---}} время
Тогда есть хотя бы <tex>2x(i) + 1</tex> работ таких, что <tex>d'_j \le d'_i < x(i) + 1</tex>.
Их невозможно сделать за <tex>x(i)</tex> времени, а значит, в каждом таком расписании есть опоздание.
}}
{{Утверждение
|about=#3
|statement=При сдвиге всех <tex>d_i</tex> на <tex>l</tex>, <tex>d'_i</tex> сдвинутся также на это число.
|proof=
Для работ, от которых ничего не зависит, по определению <tex>d'_i = d_i</tex>, а, значит, для них утверждение верно.
Рассмотрим остальные в порядке топологической сортировки. Тогда, по индукции, для всех потомков рассматриваемой вершины
утверждение будет верно. Также, так как <tex>d'_k + l \le d'_j + l \iff d'_k \le d'_j</tex>,
<tex>(d_i + l)' = \min\{d_i + l, \min\{d'_j + l - \lceil\frac{g(i, d'_j)}{2}\rceil\}\}</tex> для <tex>j \in S(i)</tex>.
Вынеся за минимум общее слагаемое, по определению вынужденных дедлайнов, получим искомую формулу <tex>(d_i + l)' = d'_i + l</tex>
}}
{{Теорема
|statement=Алгоритм строит оптимальное расписание
|proof=
Пускай каким-то образом было вычислено оптимальное значение <tex>l_{max}</tex>. Тогда, по второму утверждению, если сдвинуть все
дедлайны на <tex>l_{max}</tex>, то алгоритм получит для них оптимальное расписание.
По третьему утверждению, для любого сдвига будет получено расписание с одним и тем же опозданием. Значит,
для сдвига на <tex>l_{max}</tex> оно также будет оптимальным.
В силу того, что для любого сдвига будет построено оптимальное расписание, алгоритм находит оптимальное расписание.
}}