Рубрика «логические задачи»

Однажды попалась мне игра пентамино, где было необходимо уложить 13 фигурок в квадрат 8 на 8. После некоторого периода времени, втечение которого я безуспешно пытался решить эту задачу, я решил, что необходимо написать программу, которая бы делала это за меня. Для этого необходимо было выбрать алгоритм решения. Первое, что приходит на ум — это обычный алгоритм ветвей и границ, когда фигурки укладываются одна за другой примыкая друг к другу (алгоритм с танцующими ссылками здесь не подходит, поскольку фигурки разные). Для ускорения этого алгоритма обычно используются различные эвристики, например, предпочтение отдается ветвлению с наименьшим количеством вариантов. Можно придумать и реализовать и другие эвристики в этом алгоритме, но тут я подумал, что множество различных ухищрений для ускорения решения подобных задач уже реализовано в SAT солверах. Поэтому, необходимо перевести задачу на соответствующий математический язык и воспользоваться каким-либа SAT солвером. О том, как это было реализовано и какие получились результаты можно почитать под катом.
Читать полностью »