Добавить туда еще cuneiform или tesseract, воткнуть это в планшет: щелкнул камерой листик с кроссвордом, через некоторое время получил изображение решенного =D
То же самое забульбенить со сканвордами, судоку и японскими кроссвордами.
А еще прикола ради добавить шахматы. И играть с мужиками на баксы.
И решатель преферанса. До первых канделябр можно поиграть.
Ну если SAT (кроме prolog-ов/mercury/curry) - есть библиотеки, вот полуоткрытая (вроде) z3 популярна, еще есть открытая cvc4. Эти обе SMT, и SAT - как его чать. А так, minisat тоже вроде используется.
А finite-domain - видел в prolog-е (и curry/PAKCS который в prolog и компилится), еще где-то должен быть.