Algebraic-Attack
為什麼 SAT 求解器之間存在巨大差異？
SAT 求解器在代數攻擊中非常重要，例如walksat和minisat。
但是，當解決此處可用的基準問題時，兩者之間存在巨大的性能差異 - 對於這些問題，Walksat 比 minisat 快得多。為什麼是這樣？
walksat 的這種實施似乎有一些性能改進——它沒有被列入國際 SAT 比賽有什麼原因嗎？
Walksat 是一個不完全求解器。這意味著它試圖為多次迭代找到解決方案。如果它確實找到了解決方案，它會回答該解決方案，否則它會回答“不知道”。Walksat 使用一種隨機遊走形式來搜尋具有啟發式的解決方案來指導其步驟。
另一方面，如果有足夠的計算資源，Minisat 會為您提供解決方案或問題無法滿足的答案（並且通過添加證明跟踪，您還可以獲得證明）。Minsat 使用現代形式的DPLL。
對您的問題的簡短回答是，搜尋答案（如果存在）比證明不存在答案更容易。
更長的答案是，只有當有很多解決方案並且它們的結構在搜尋空間中屬於特殊類型時，walksat 才會比 minisat 快。
在帶有基準的頁面上，我找不到對 walksat 的任何參考。你有沒有自己測試過一些基準測試？您是否在已知無法滿足的基准上測試過 walksat？