Без заголовка

Делают, просто в университетских проектах в основном. По ним даже соревнования проводят. Типа какой солвер решит больше Constraint Satisfaction Problem. Ханойская башня - это что-то вроде Хэлло Ворлд для таких методов, то есть одна из учебных програм. Не так давно и SAT-solverы стали применять для решения CSP задач, теоретически такая возможность была рассмотрена в начале 2000, я так понимаю. В презентации по SAT4J - Java SAT-Solver - тоже есть пример про ханойские башни. Ну т.е. в данном случае они вполне в общей струе. А вот почему в практических проектах это редко применяют, это другой вопрос. Я к примеру пытаюсь, но на мелких проектах овчинка выделки не стоит, проще ручками. Хотя, лично для меня, есть весьма полезный косвенный эффект в лучшем понимании требований. Кроме того, отмечу, что на практике, алгоритм должен работать предсказумое время, а у САТ-солверов с этим напряженка: в большинстве случаев может они и справятся за разумное время, но возможны подвисания. Для обычных программ это редко примелимо, ибо пользователь будет на уши ставить всех из-за таких подвисонов.