Работа посвящена решению задачи сапера как задачи программирования в булевых ограничениях и разработке модуля автоматизированного решения задачи сапера с использованием бинарных решающих диаграмм. Реализованный модуль включает в себя пользовательский интерфейс, формирование булевых функций на основе фактов о расположении мин и интерпретацию максимально сильного следствия из фактов. Для представления булевых функций и последующей работы с ними были использованы бинарные решающие диаграммы. Модуль решения задачи сапера предназначен для интеграции на национальную платформу «Открытое образование» в качестве пособия для слушателей курса профессора Карпова «Математическая логика», чтобы продемонстрировать слушателям курса, что полученной ими информации достаточно для того, чтобы запрограммировать самим логическую задачу.

• Список обозначений
• Введение
• Задача «Сапер» как логическая игра
  • 1.1 Дистанционный курс «Математическая логика» и задача «Сапер»
    • 1.1.1 Особенности дистанционного курса «Математическая логика»
    • 1.1.2 «Основные понятия логики высказываний» и задача «Сапер»
  • 1.2 Уточненная постановка задачи
• Решение задачи «Сапер» как задачи программирования в булевых ограничениях
  • 2.1 Программирование в логических ограничениях
  • 2.2 Логические ограничения для задачи «Сапер»
  • 2.3 Бинарные решающие диаграммы
• Реализация модуля автоматизированного решения задачи «Сапер»
  • 3.1 Библиотеки Swing и AWT
  • 3.2 Пользовательский интерфейс приложения «Интеллектуальный сапер»
  • 3.3 Библиотека JavaBDD
  • 3.4 Автоматизированное решение задачи «Сапер»
  • 3.5 Результаты тестирования приложения «Интеллектуальный сапер»
• Заключение
• Литература