Verification of backtracking and branch and bound design templates
Nikolay V. Shilov · Automatic Control and Computer Sciences · 2012
The design and analysis of computer algorithms is a requirement of computer curricula. It covers many topics, including data structures, complexity theory, and algorithmic design patterns. This course is about the greedy method, divide and conquer, dynamic programming, backtracking, and branch and bound. Naturally, all the listed design patterns are taught, learned, and comprehended using examples. However, they can be semiformalized as design templates, specified by correctness conditions, and manually verified by means of the Floyd method. Moreover, this approach can lead to new insights and better comprehension of the design patterns, specifications, and verification methods. In this paper, we demonstrate the utility of the approach using the study of the backtracking and branch-and-bound design patterns. In particular, we prove the correctness of the suggested templates when the boundary condition is monotone, but the decision condition is antimonotone on sets of “visited” vertices.