В работе рассматриваются вопросы логической формализации и решения задач с использованием автоматических систем проверки выполнимости. Предлагается автоматический транслятор 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.