Kryptoanaliza oparta na SAT
Przełożenie szyfru na ogromną formułę boolowską i zlecenie solwerowi SAT poszukiwania klucza.
Fabio Massacci i Laura Marraro nazwali to kryptoanalizą logiczną, gdy w 2000 roku zakodowali DES jako problem spełnialności. Przy kilku rundach solwer znalazł klucz; przy pełnym DES-ie się poddał, zgodnie z oczekiwaniami. Podejście jest bliskim krewnym ataków algebraicznych, ale zamienia wielomiany na klauzule i korzysta z dziesięcioleci inżynierii znanej z weryfikacji sprzętu.
Przełom był praktyczny, nie teoretyczny. W 2006 roku Mironov i Zhang użyli solwerów SAT do zautomatyzowania części poszukiwania kolizji dla MD4 i MD5, a Mate Soos zbudował CryptoMiniSat z natywną obsługą XOR, ulubionej operacji projektantów szyfrów. Dziś najczęściej solwer szuka najlepszej charakterystyki różnicowej dla kogoś, kto projektuje nowy szyfr – a nie łamie stare.