В работе рассматривается история семинара «Проблемы сокращения перебора» в ЛЭТИ, организованного Р. И. Фрейдзоном (1942-2018). Семинар начал свою работу в 1982 г., ставя в первую очередь своей целью развитие идей С. Ю. Маслова (1939-1982), и действовал до начала 1990-х годов. Историко-научный контекст, рассматриваемый в работе, включает связи этого семинара с другими семинарами - семинаром С. Ю. Маслова, семинаром по математической логике в ЛОМИ им. В. И. Стеклова, круг идей, рассматривавшихся на семинаре и основные результаты его деятельности, выразившиеся в научных публикациях его участников. Рассматриваются также научно-педагогические аспекты деятельности семинара (его роль в формировании молодых ученых), организационная деятельность Р. И. Фрейдзона и влияние его личности на творческую атмосферу, окружавшую семинар. С. 5-14.

The paper discusses the history of the seminar “Problems of Reducing the Exhaustive Search” organized at the Leningrad Electrotechnical Institute (LETI) by R. I. Freidson pagebreak (1942-2018). The seminar began its work in 1982, setting as its primary goal the development of the ideas of S. Yu. Maslov (1939-1982), and its work continued until the beginning of the 1990s. The historical and scientific context considered in this work, includes the links of this seminar with other seminars, such as S. Yu. Maslov’s seminar and the seminar on mathematical logic at the Leningrad Branch of the Steklov Mathematical Institute (LOMI) along with the ideas developed at the seminar and the main results of its activity expressed in the scientific publications. Also considered are the scientific and pedagogical aspects of the seminar (its formative influence on young scientists), the organizational activities of R. I. Freidson and the influence of his personality on the creative atmosphere surrounding the seminar.

В работе рассматриваются вопросы логической формализации и решения задач с использованием автоматических систем проверки выполнимости. Предлагается автоматический транслятор TouIST, который позволяет генерировать логические формулы на основе простого полуформального описания проблемы. С его помощью оказывается возможным моделировать множество статических и динамических комбинаторных задач. Подчеркивается полезность системы в качестве вспомогательного средства для сопровождения курса логики и дискретной математики. Дополнительную выгоду пользователи смогут извлечь благодаря постоянному совершенствованию SAT, QBF и SMT-систем проверки выполнимости применительно к эффективному решению конкретных логических и комбинаторных проблем, таких, как планирование задач в области искусственного интеллекта. С. 13-25. (на англ.)

This work deals with logical formalization and problem solving using automated solvers. We present the automatic translator TouIST that provides a simple language to generate logical formulas from a problem description. Our tool allows us to model many static or dynamic combinatorial problems. All this can be very helpful as a teaching support for logics and discrete mathematics. Users will benefit from the regular improvements of SAT, QBF or SMT solvers in order to solve concrete logical and combinatorial problems efficiently, e.g., different classes of planning tasks in Artificial Intelligence.