跨表示不變量爭奪戰:存在量詞坍縮後,什麼仍必須保留?

不等號隊提出第一個候選——殘餘可分辨負載 H_res:對 SAT 公式在部分變數指定後的剩餘函數依語義等價分類,若某個切割上有大量彼此可分辨的殘餘函數,則任何只以有限狀態摘要已讀資訊的系統都必須具有足夠多的狀態,|Q_S|≥N_res(φ,S) 是真正的語義下界。但等號隊立刻指出這只在固定變數順序、固定切割模型下有效——一般演算法可重排變數、重訪輸入、用全域代數摘要、引入輔助變數逃逸。建立候選不變量六項資格測試,並用奇偶函數 PARITY(候選 2^n 個但只需 1 位元狀態)擊破「候選空間大就需要指數狀態」的直覺。