Geodesic
Verification of backtracking and branch and bound design templates
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 168-180.

Voir la notice de l'article provenant de la source Math-Net.Ru

The Design and Analysis of Computer Algorithms is a must of Computer Curricula. It covers many topics that group around several core themes. These themes range from data structures to the complexity theory, but one very special theme is algorithmic design patterns, including greedy method, divide-and-conquer, dynamic programming, backtracking and branch-and-bound. Naturally, all the listed design patterns are taught, learned and comprehended by examples. But they can be semi-formalized as design templates, semi-specified by correctness conditions, and semi-formally verified by means of Floyd method. Moreover, this approach can lead to new insights and better comprehension of the design patterns, specification and verification methods. In this paper we demonstrate an utility of the approach by study of backtracking and branch-and-bound design patterns. In particular, we prove correctness of the suggested templates when the boundary condition is monotone, but the decision condition is anti-monotone on sets of “visited” vertices.
Keywords: backtracking, branch-and-bound, abstract data type, partial correctness, total correctness, Floyd proof method, $n$-queen puzzle, knapsack problem. 
@article{MAIS_2011_18_4_a14,
     author = {N. V. Shilov},
     title = {Verification of backtracking and branch and bound design templates},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {168--180},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a14/}
}
TY  - JOUR
AU  - N. V. Shilov
TI  - Verification of backtracking and branch and bound design templates
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 168
EP  - 180
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a14/
LA  - ru
ID  - MAIS_2011_18_4_a14
ER  - 
%0 Journal Article
%A N. V. Shilov
%T Verification of backtracking and branch and bound design templates
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 168-180
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a14/
%G ru
%F MAIS_2011_18_4_a14
N. V. Shilov. Verification of backtracking and branch and bound design templates. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 168-180. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a14/

[1] A. Akho, Dzh. Khopkroft, Dzh. Ulman, Postroenie i analiz vychislitelnykh algoritmov, Mir, M., 1979 | MR

[2] D. Gris, Nauka programmirovaniya, Mir, M., 1984

[3] V. E. Deikstra, Distsiplina programmirovaniya, Mir, M., 1978

[4] T. Kornmen, Ch. Leizerson, R. Rivest, Algoritmy: postroenie i analiz, MTsNMO, M., 2000

[5] V. A. Nepomnyaschii, “Verifikatsiya finitnykh iteratsii nad naborami izmenyaemykh struktur dannykh”, Kibernetika i sistemnyi analiz, 2007, no. 3, 33–46

[6] N. V. Shilov, Osnovy sintaksisa, semantiki, translyatsii i verifikatsii programm, Novosibirskii gosudarstvennyi universitet, Novosibirsk, 2011

[7] K. R. Apt, F. S. de Boer , E. R. Olderog, Verification of Sequential and Concurrent Programs, Third edition, Springer, 2009

[8] R. W. Floyd, “Assigning meanings to programs. Proc. of a Symposium in Applied Mathematics. Mathematical Aspects of Computer Science”, J. American Math. Society, 19 (1967), 19–32, Providence, R.I. | MR | Zbl

[9] S. W. Golomb, L. D. Baumert, “Backtrack Programming”, Journal of ACM, 12(4) (1965), 516–524 | DOI | MR | Zbl

[10] A. H. Land, A. G. Doig, “An automatic method of solving discrete programming problems”, Econometrica, 28(3) (1960), 497–520 | DOI | MR | Zbl

[11] E. Kant, “Understanding and Automating Algorthm Design”, IEEE Transactions on Software Engineering, SE-11(11) (1985), 1361–1374 | DOI

[12] D. R. Smith, “Automating the design of algorithms”, Formal Program Development, Lecture Notes in Computer Science, 755, 1993, 324–354