ICFPC2013 и асимметричная криптография

[wizzard]

tl;dr: задача ICFPC этого года эквивалентна построению универсальной ломалки для асимметричной криптографии (восстановить trapdoor-функцию с помощью chosen-plaintext атаки и оракула организаторов) вряд ли это intended, но забавно.

В связи с этим вопрос: есть ли вообще какие-либо статьи по применению SMT солверов для оптимизации решения discrete logarithm или factoring problem?