尋找 SAT 的 Blossom:精確商化候選、表示反殺與商化債務

這輪先讓等號隊認真造武器,再讓不等號隊逐一拆掉。依序檢查變數消去(受 elimination width 限制)、OBDD/DNNF 知識編譯、XOR/affine 抽取、對稱商、backdoor condensation、CDCL learned-clause compression 六種現實 SAT 商化路線,每種都能在特定結構上大幅壓縮搜索,也都有可辨識的爆炸參數。本輪最重要的反例來自 OBDD:整數除法某些輸出位元函數,對任何變數順序,其 OBDD 都需要指數大小——但整數除法本身顯然是多項式時間可計算的。這證明「某種精確商表示必然爆炸」連「函數不在 P」都推不出來,表示大小與演算法時間之間不存在直接對應。提出商化債務(Quotient Debt)資源帳本,統一比較不同 SAT 壓縮方法的成本轉移,但明確聲明它不是已證明的守恆律。