Солвер — это инструмент, который позволяет задать систему неравенств и прочих условий, и на выходе дать решение, которое удовлетворяет этой системе. По сути, это декларативное программирование, когда нам вообще не важно, как это будет работать, главное — результат.

Я еще несколько месяцев назад наискосок просмотрел немного документации (раз и два), но к практике на основе репозитория в итоге перешёл только в поезде без интернета, поэтому первые два задания я подглядел. В остальном все решалось достаточно просто, для решения задач нужно совсем немного конструкций.

В целом сама парадигма довольно прикольная: надушить четкое ТЗ и дело в шляпе (а недостаточно душнишь — держи тривиальное решение с нулями). Какое-нибудь судоку решать с помощью него — самое то, фигачится минут за 10. Да и задача о рюкзаке была реализована мной за примерно такое же время — это не динпрог вертеть.

Однако чудес солвер тоже не открыл. Магический квадрат для 4x4 он находит мгновенно, а вот 5x5 уже не смог (я не стал ждать больше 10 минут). При этом проц и память были вообще не нагружены, т.е. по умолчанию параллелизации нет. И рюкзак для «плохих» входных данных (где стоит приближенно решать) тоже быстро не отработал.

В общем, для чего-то простого, когда может человек решить с ручкой и бумагой за обозримое время или программист тупым перебором — вполне достойный вариант. Но если известен хороший алгоритм и задача не одноразовая, то стоит посмотреть альтернативы.