论文标题
发现和认证在线垃圾箱拉伸问题的下限
Discovering and Certifying Lower Bounds for the Online Bin Stretching Problem
论文作者
论文摘要
在线计算理论中有几个问题，竞争比率的紧密下限是未知的，预计将很难以短形式描述。一个很好的例子是在线垃圾箱拉伸问题，其中任务是将传入的物品在线包装成垃圾箱，同时最大程度地减少最大垃圾箱的负载。另外，整个实例的最佳负载是事先已知的。 本文的贡献是双重的。我们使用COQ证明助手正式化在线垃圾箱拉伸问题，并提供一个证明此问题下限的程序。由于证书的规模，先前声称的下限从未正式证明。据我们所知，这是首次使用正式验证工具包来证明在线问题的下限。 我们还为在线垃圾箱提供了第一个非平凡的下限，并使用6、7和8个垃圾箱提供了最著名的下限，并增加了最著名的下限3箱。我们详细描述了发现新的下限所必需的算法改进，这是几个数量级更复杂的顺序。
There are several problems in the theory of online computation where tight lower bounds on the competitive ratio are unknown and expected to be difficult to describe in a short form. A good example is the Online Bin Stretching problem, in which the task is to pack the incoming items online into bins while minimizing the load of the largest bin. Additionally, the optimal load of the entire instance is known in advance. The contribution of this paper is twofold. We use the Coq proof assistant to formalize the Online Bin Stretching problem and provide a program certifying lower bounds of this problem. Because of the size of the certificates, previously claimed lower bounds were never formally proven. To the best of our knowledge, this is the first use of a formal verification toolkit to certify a lower bound for an online problem. We also provide the first non-trivial lower bounds for Online Bin Stretching with 6, 7 and 8 bins, and increase the best known lower bound for 3 bins. We describe in detail the algorithmic improvements which were necessary for the discovery of the new lower bounds, which are several orders of magnitude more complex.
