Меня эта задача (SAT) тоже интересует, я занимался довольно плотно одно
время, надеялся на конкурс RSA пролезть
во - http://nishi.dreamhosters.com/u/multest1a.png
Это система для факторизации чисел, на базе моей старой реализации.
Ну, там задано просто умножение двух чисел, результат которого равен
константе, и солвер должен найти множители (с некоторыми доп.условиями там
единственное решение).

А еще я хочу ломалку зипкрипта сделать на базе этого.
Там же есть возможность по контрольным суммам ломать шифрование без тупого перебора.
Пока сделал только простой крэкер с тупым перебором - http://nishi.dreamhosters.com/u/zcrack_v0.rar :)
Там зашифрован рандомный паддинг в начале файла, а в этот паддинг обычно
вставляется 16 или 8 (по новому стандарту) битов crc32 файла.
Причем инициализация ключа - функция типа сишного рандома, т.е. не
криптохэш совсем.
Ну а в идеале можно и сам рандом приплести, которым паддинг генерируется,
но это надо конкретные реализации зипа смотреть.

В принципе, для меня как раз хорошо, что там не настоящая криптография,
т.к. есть шанс реально это решить, а то даже для md5 несколько не те
мощности нужны, какие у меня есть.

Изначально я вообще пытался в математику это перевести
там можно через модульную арифметику типа (a+b) mod 2 = a xor b
можно через a*b=AND(a,b), a+b-a*b=OR(a,b)
(это довольно интересно - получаются офигенные полиномы),
можно через тригонометрию, как вариант модульной арифметики
Просто я тогда еще верил в продвинутость разработчиков системы mathematica :), 
поэтому пытался некоторое время логические системы транслировать в
решение понятных ей задач, и смотрел, что выйдет - оказалось, что плохо
выходит :)

У меня была математика 2.0 (wolfram mathematica) под дос,
мне просто случайно повезло - у меня на подработке работал физик из универа,
который этой математикой считал себе что-то для статей.
Он ее со штатов привез, по-моему даже купленную.