Automated bounds on recursive structures

Abstract

Tables are the basis for many dynamic programming algorithms on recursive structures such as trees and grids. These tables record the rules for combining structures. We show how such a table can be used to determine the maximum or minimum value of the associated parameter (the extremal function), and implement software that automatically determines the extremal function from the table, and outputs a proof thereof. We also produce software that automatically generates a candidate table from a black-box oracle for the parameter. We use the software to solve some old and new problems; for example, we obtain the values of domination parameters for some small grids.