调度问题贪心算法A的最优性形式化证明技术问询

问题背景 #

给定一组事件，每个事件包含截止日期d和持续时长l天。目标是设计算法选出尽可能多的事件，需满足以下约束：

• 每个事件必须在截止日期d前完成，且需连续占用l天；
• 同一时间只能执行一个事件。

贪心算法A的具体实现 #

创建最大堆 S  // 存储当前调度计划

将所有事件按截止日期递增排序

for(j=0;j<events.size();j++)
{ 
  若事件j可加入当前调度S，则直接加入；
  否则，若S中时长最长的事件 > 事件j的时长，则将两者交换；
}

返回 S; 
END

证明瓶颈 #

目前已确定存在按截止日期递增顺序执行的最优调度方案O，但无法通过形式化方法证明算法中“替换最长事件”的操作最终会收敛到最优解，因此无法完成该贪心算法最优性的完整证明。

内容的提问来源于stack exchange，提问作者Ajax