Aes
AES可以通過減少到SAT來解決嗎？
考慮一個已知的對 AES 的明文攻擊——這樣我們就有了一個實際的等式系統，我們可以將它提供給 SAT 求解器。
AES可以通過這種方式解決嗎？換句話說，算法最終會完成，產生正確的密鑰嗎？
閱讀完這組幻燈片後，我認為答案是肯定的，但它在計算上比蠻力更昂貴，因此不切實際。
AES可以通過這種方式解決嗎？換句話說，算法最終會完成，產生正確的密鑰嗎？
幾乎是的。它會產生一些正確的密鑰——可能不止一個。
（給定“足夠的”明文-密文樣本，它應該很可能是唯一的，但通常情況並非如此。）
通常，在已知明文場景中計算密鑰是 $ \mathbf{NP} $ ，因此根據定義可以簡化為任何 $ \mathbf{NP} $ - 完整的問題，例如 $ \mathrm{SAT} $ . 如果正確完成，解決 $ \mathrm{SAT} $ instance 必然會產生正確的密鑰——但幸運的是，就我們目前所知，這樣做根本不切實際。
（如果事實證明 $ \mathbf P=\mathbf{NP} $ ，這可能會稍微改變那幅畫，但在這種情況下，無論如何我們都注定要失敗。）
因此，簡短的回答是：是的，但這無濟於事。