SAT 求解器（SAT solver）

SAT 求解器回答一個看似簡單的問題：給定一個布林公式——由許多 OR 子句以 AND 串起、變數取真／假——是否存在某種變數指派能讓整個公式為真？它是最初的 NP-complete 問題，所有難度的標竿，然而現代 SAT 求解器卻能例行地破解擁有數百萬變數的公式。在晶片設計裡，它是等價檢查、有界模型檢查、ATPG 測試生成、乃至可被編碼成「這條限制可滿足嗎？」的繞線與時序難題背後的主力。

其引擎是 CDCL——衝突驅動子句學習：猜某個變數的值，傳播被強制的後果（單元傳播），當撞上矛盾時，分析它「為何」發生，學到一條永遠禁止這個錯誤的新子句，再回跳重試。兩個點子讓它威力大增：以活躍度為基礎的聰明分支（VSIDS），專注於近期常惹麻煩的變數；以及監看文字（watched-literal）資料結構，讓傳播快如閃電。SAT 及其更豐富的表親 SMT，已悄悄取代許多以 BDD 為基礎的流程，因為它們能擴展到 BDD 會爆炸的設計規模。