Верификация шаблонов алгоритмов для метода отката и метода ветвей и границ


https://doi.org/10.18255/1818-1015-2011-4-168-180

Полный текст:


Аннотация

Курс проектирования и анализа алгоритмов является обязательной составляющей учебных программ по информатике всех уровней. В университетах этот курс обязательно включает изучение структур данных, методы проектирования алгоритмов, теорию сложности и т.д. Этот курс знакомит с такими методами проектирования алгоритмов, как жадные алгоритмы, динамическое программирование, метод разделяй и властвуй, метод отката, метод ветвей и границ. Обычно знакомство с этими методами происходит на примерах. Но (как показано в данной статье) они могут быть (полу)формализованы в виде "паттернов", специфицированы условиями частичной и/или тотальной корректности и обоснованы (доказаны) методом Флойда верификации алгоритмов. Такой формализованный подход может привести к новому, более глубокому пониманию этих методов. В статье демонстрируется перспективность такого подхода на примере метода отката и метода ветвей и границ. В частности, мы доказываем, что разработанные шаблоны корректны, если граничное условие - монотонная функция, а решающее условие - антимонотонная функция от множества уже проверенных вершин.

Об авторе

Николай Вячеславович Шилов
Институт систем информатики им. А.П. Ершова СО РАН, Новосибирский государственный университет и Новосибирский государственный технический университет
Россия


Список литературы

1. Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир, 1979.

2. Грис Д. Наука программирования. М.: Мир, 1984.

3. Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.

4. Корнмэн Т, Лейзерсон Ч, Ривест Р. Алгоритмы: построение и анализ. М.: МЦНМО, 2000.

5. Непомнящий В.А. Верификация финитных итераций над наборами изменяемых структур данных. Кибернетика и системный анализ. Киев. 2007. №3. С.33-46.

6. Шилов Н.В. Основы синтаксиса, семантики, трансляции и верификации программ. Новосибирск: Новосибирский государственный университет, 2011.

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

8. Floyd R.W. Assigning meanings to programs. Proc. of a Symposium in Applied Mathematics. Mathematical Aspects of Computer Science // American Math. Society, Providence, R. I. 1967. Vol. 19. P. 19-32.

9. Golomb S.W. and Baumert L.D. Backtrack Programming // Journal of ACM. 1965. 12(4). P. 516-524.

10. Land A. H. and Doig A. G. An automatic method of solving discrete programming problems // Econometrica. 1960. 28(3). P. 497-520.

11. Kant E. Understanding and Automating Algorthm Design // IEEE Transactions on Software Engineering. 1985. SE-11(11). P. 1361-1374.

12. Smith D. R. Automating the design of algorithms // Formal Program Development. 1993. Lecture Notes in Computer Science. 755. P. 324-354.


Дополнительные файлы

Для цитирования: Шилов Н.В. Верификация шаблонов алгоритмов для метода отката и метода ветвей и границ. Моделирование и анализ информационных систем. 2011;18(4):168-180. https://doi.org/10.18255/1818-1015-2011-4-168-180

For citation: Shilov N.V. Verification of Backtracking and Branch and Bound Design Templates. Modeling and Analysis of Information Systems. 2011;18(4):168-180. (In Russ.) https://doi.org/10.18255/1818-1015-2011-4-168-180

Просмотров: 5

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)