An automatic verifier for the feasibility of special cases of the offline dynamic storage allocation problem

The offline Dynamic Storage Allocation (DSA) problem is a well-known problem in combinatorial optimization. The problem is one of packing a set of blocks of arbitrary sizes on an area, with the objective of minimizing the area´s usage along the y-axis, under the condition that the x-position of the blocks are fixed (as given in the input). The problem has uses in memory management, berth allocation, and can potentially be used in the allocation of bandwidth resources in a network. Li et al. [4] considered the case of the problem where the width of the blocks (their dimension along the y-axis) is to be no larger than a given number. They obtained several approximation algorithms for special cases of the problem, by first studying the feasibility of several subcases with further restriction, such as limiting the y-dimension of the area to pack the blocks. We believe that such feasibility results on subcases of the problem can help in obtaining algorithms for other special cases of the problem. In this paper we propose a method to automatically derive such results. Our implementation of a simplified version of the proposed method in C++ correctly duplicated many of the earlier results obtained by Li et al.