Потыкал немного в MiniZinc, язык для формулировки и решения проблем с ограничениями. В общем, довольно удобная штука, определяешь переменные и связи между ними на достаточно простом и гибком языке (есть поддержка целых чисел, плавающей точки, строк, массивов и множеств). Потом это компилируется в какую-то стандартную форму и скармливается программе-решателю (finite domain constraint solver), которых есть много разных, три поставляются вместе с самим MiniZinc. Чем эти решатели отличаются друг от друга и от SAT-решателей, я решительно не знаю, похоже, за последние 20 лет там наворотили кучу прогресса.
Не очень ясно, для каких серьезных вещей это нужно (но уверен, что есть такие, и кому надо - знают). Для всяких игрушечных целей это использовать легко и приятно, после первичной ассимиляции незнакомых понятий. Но надо помнить, что это не магия, в конечном итоге если будет много независимых переменных и слабые связи, он ничего не найдет. Скажем, для сравнения: найти расстановку 8 неатакующих ферзей на шахматной доске с помощью этого языка очень легко (и думаю, посчитать число решений тоже), а вот найти обход коня, покрывающий всю доску, наверное, невозможно - моя программа нашла обход длиной 30 за 15 секунд, а обход длиной 40 я устал ждать.
Всякого рода комбинаторные задачки, которые предназначены для решения вручную, можно щелкать как орешки. Вот для примера моя программа для решения следующего ребуса: МОРЕ+ШТОРМ=АВАРИЯ. https://pastebin.com/VeTXRQmg
Кстати, непростой ребус для решения вручную, попробуйте, если интересно (нужно найти, как заменить буквы на цифры, чтобы сложение было верным, при этом одной букве соответствует всегда одна и та же цифра, и разным буквам разные цифры). Я решал его вместе с женой и дочкой вчера, и у нас оказалось два разных решения. Я этой программой заодно проверил, есть ли еще, и нет - есть ровно два разных решения ребуса.
