Finite-Basis Theorems and a Computation-Integrated Approach to Obstruction Set Isolation

Recent advances in well-partial-order theory, especially the seminal contributions of Robertson and Seymour, make tools available that establish only the existence of polynomial-time decision algorithms. The finite-basis theorems that are the engine of these developments are inherently nonconstructive, providing no effective means for capturing the obstruction sets on which these polynomial-time algorithms are based. In this paper, we use a well-studied matrix permutation problem to describe an approach to obstruction set isolation that makes essential use of the computer in a mathematical proof. (In fact, the task of identifying such obstruction sets appears to pose many “4CT-like” problems for which computational assistance is vital.) We also discuss an approach based on a computational “learning” paradigm that incorporates a fundamental component of computer-aided obstruction identification with self-reduction to obtain known polynomial-time algorithms that do not depend on the knowledge of an entire obstruction set.