В данной работе изложен подход к разработке обучающего тренажера для студентов, изучающих математическую логику и испытывающих трудности с построением бинарных решающих диаграмм. Основным методом построения тренажера является агент, который посредством логического вывода решает задачу «Сапер» как задачу программирования в ограничениях. Для этого предварительно все ограничения в задаче «Сапер» были формализованы с помощью логики высказываний, и все булевы функции представлены в виде бинарной решающей диаграммы. Программная часть реализована в среде моделирования AnyLogic, и в связи с этим написана полностью на языке программирования Java. Для представления в программе булевых функций в виде бинарных решающих диаграмм была использована сторонняя библиотека JavaBDD. В результате, был разработан тренажер, оперирующий логическим агентом, который автоматизированно решает задачу «Сапер» с использованием бинарных решающих диаграмм. На каждом ходе агента от обучающегося требуется ввести функцию-ограничение, соответствующее текущей ситуации на карте. Функция задается с помощью списочного представления бинарной решающей диаграммы. Она автоматически проверяется. По результатам проверки, тренажер выдает информацию о том, корректно ли было введенное обучающимся ограничение.

This thesis examines an approach to development of an educational game for students studying mathematical logic and having difficulty with binary decision diagrams. The main method that the educational game uses is an agent that solves the Minesweeper problem as constraint satisfaction problem using logical inference. All constraints in the Minesweeper problem were formalized beforehand in propositional calculus and every Boolean functions are represented in binary decision diagrams. The game is developed in AnyLogic Simulation Software and therefore, written in Java programming language. For representing Boolean functions as BDD, a third-party library JavaBDD was used. As a result, an educational game was developed that has a logical agent that automatically solves the Minesweeper problem using binary decision diagrams. With every step of agent, the student is required to insert the constraint function that lines up with certain state on a field. This function is defined by a table representation of the BDD, and then it is automatically checked. Consequentially, the game informs the student whether the inserted data was correct.