Discovering and certifying lower bounds for the online bin stretching problem. (English) Zbl 1540.68325
Summary: 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.
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.
MSC:
| 68W27 | Online algorithms; streaming algorithms |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 90C27 | Combinatorial optimization |
References:
| [1] | Azar, Y.; Regev, O., On-line bin-stretching, Theor. Comput. Sci., 268, 1, 17-41 (2001) · Zbl 0984.68195 |
| [2] | Kellerer, H.; Kotov, V.; Speranza, M. G.; Tuza, Z., Semi on-line algorithms for the partition problem, Oper. Res. Lett., 21, 5, 235-242 (1997) · Zbl 0908.90165 |
| [3] | Böhm, M.; Sgall, J.; van Stee, R.; Veselý, P., Better algorithms for online bin stretching, (International Workshop on Approximation and Online Algorithms (2014), Springer), 23-34 · Zbl 1457.68314 |
| [4] | M. Gabay, N. Brauner, V. Kotov, Computing lower bounds for semi-online optimization problems: application to the bin stretching problem, HAL preprint hal-00921663, version 2 (2013). |
| [5] | Gabay, M.; Brauner, N.; Kotov, V., Improved lower bounds for the online bin stretching problem, 4OR, 15, 2, 183-199 (2017) · Zbl 1369.90073 |
| [6] | Böhm, M.; Sgall, J.; van Stee, R.; Veselý, P., Online bin stretching with three bins, J. Sched., 20, 6, 601-621 (2017) · Zbl 1390.90307 |
| [7] | Böhm, M., Online bin stretching: Algorithms and computer lower bounds (2018), Ph.D. thesis |
| [8] | Blum, M.; Kannan, S., Designing programs that check their work, J. ACM, 42, 1, 269-291 (1995) · Zbl 0886.68046 |
| [9] | Mehlhorn, K.; Näher, S.; Uhrig, C., The LEDA platform for combinatorial and geometric computing, (International Colloquium on Automata, Languages, and Programming (1997), Springer), 7-16 |
| [10] | Alkassar, E.; Böhme, S.; Mehlhorn, K.; Rizkallah, C., A framework for the verification of certifying computations, J. Autom. Reason., 52, 3, 241-273 (2014) · Zbl 1314.68180 |
| [11] | Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: a Proof Assistant for Higher-Order Logic, vol. 2283 (2002), Springer Science & Business Media · Zbl 0994.68131 |
| [12] | McConnell, R. M.; Mehlhorn, K.; Näher, S.; Schweitzer, P., Certifying algorithms, Comput. Sci. Rev., 5, 2, 119-161 (2011) · Zbl 1298.68289 |
| [13] | Abdulaziz, M.; Mehlhorn, K.; Nipkow, T., Trustworthy graph algorithms (2019), CoRR · Zbl 1541.68266 |
| [14] | Noschinski, L., Formalizing graph theory and planarity certificates (2016), Technische Universität München, Ph.D. thesis |
| [15] | Rizkallah, C., An axiomatic characterization of the single-source shortest path problem, Arch. Formal Proofs (May 2013) |
| [16] | Barras, B.; Boutin, S.; Cornes, C.; Courant, J.; Filliatre, J.-C.; Gimenez, E.; Herbelin, H.; Huet, G.; Munoz, C.; Murthy, C., The Coq Proof Assistant Reference Manual: Version 6.1 (1997) |
| [17] | Böhm, M., binstretch: computing lower bounds for Online Bin Stretching in C++, github code repository |
| [18] | Böhm, M.; Simon, B., LBBinStretching: certifying lower bounds for Online Bin Stretching, github code repository |
| [19] | Zobrist, A. L., A new hashing method with application for game playing (1970), Technical Report 88 |
| [20] | Gabriel, E.; Fagg, G. E.; Bosilca, G.; Angskun, T.; Dongarra, J. J.; Squyres, J. M.; Sahay, V.; Kambadur, P.; Barrett, B.; Lumsdaine, A., Open mpi: goals, concept, and design of a next generation mpi implementation, (European Parallel Virtual Machine/Message Passing Interface Users’ Group Meeting (2004), Springer), 97-104 |
| [21] | Böhm, M., Lower bounds for online bin stretching with several bins, (SOFSEM (Student Research Forum Papers/Posters) (2016)), 1-12 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
