# P/NP 辯論遊戲研究區｜第四輪

## 局部—全域障礙與表示逃逸：全域耦合真的等於計算困難嗎？

**Round 04: Local–Global Obstruction and Representation Escape**

- **主導研究者：** Neo.K（許筌崴）
- **協作整理：** Aletheia
- **機構：** EveMissLab（一言諾科技有限公司）
- **日期：** 2026 年 8 月 1 日
- **版本：** v1.0
- **研究狀態：** 第四輪雙假設預演
- **前置文件：**
  - `00_數學構造狀態機中介層_v1.0.md`
  - `01_第一輪_存在量詞狀態坍縮.md`
  - `02_第二輪_跨表示不變量爭奪戰.md`
  - `03_第三輪_演算法軌跡切割與因果瓶頸.md`
- **遊戲態度：** 等號隊與不等號隊互相拆台
- **文件標準：** 所有數學結論仍依正式研究規格記錄；比分不是證據

---

## 摘要

第三輪將研究焦點由單純資訊量轉向「因果重建複雜度」（Causal Reconstruction Complexity, CRC）：輸入資訊即使始終存在，將其重組成精確全域答案的結構轉換仍可能昂貴。第四輪進一步詢問：這種重建成本是否可由「局部一致、全域矛盾」的耦合結構提供來源？

本輪以 Tseitin 奇偶約束作為核心思維實驗。對連通圖上的奇偶約束系統，若總 charge 為奇數，整體系統不可滿足；然而對任一頂點，存在賦值可滿足其他所有頂點的奇偶約束。故其具有極強的局部—全域落差：任何缺少至少一個頂點約束的子系統都可滿足，而完整系統卻矛盾。對展開圖上的 Tseitin CNF，解析證明（resolution）及若干受限證明系統存在強下界，顯示某些局部推理模型確實必須付出巨大代價。

但等號隊立即提出致命反例：Tseitin 約束本質上是 $\mathbb F_2$ 上的線性方程組。將所有方程相加，每條邊變數出現兩次而消去；若右側總 parity 為 $1$，便直接得到

$$
0=1.
$$

更一般地，線性方程模二可由高斯消去在多項式時間求解。因此，「局部一致性很強、全域才出現矛盾」並不推出一般計算困難；一個新的代數表示可能把原本需要長局部推導的耦合一次性壓縮成短全域不變量。

本輪因此淘汰「局部—全域落差本身就是 $P\neq NP$ 的障礙」這一過強命題，並提出新的研究方法：**表示逃逸錦標賽（Representation Escape Tournament）**。對每個候選困難實例族，不再只測一種算法或證明系統，而是用邏輯、代數、圖分解、頻譜、擴展表示等多種基底逐一攻擊。若某一表示能多項式壓縮，該實例族便不能作為跨表示硬度的直接證據。

第四輪的核心收斂是：真正需要尋找的不是「全域耦合是否存在」，而是「是否存在無法被任何有效數學表示低成本消去的**表示抗性耦合核心**」。然而若直接對所有可能表示取最小成本，定義又會循環回 $P/NP$ 本身。因此下一輪將先建立有限、可擴張的表示逃逸矩陣，透過多個經典困難族與多種算法語言進行對抗，尋找不同下界現象可能共享的更深結構。

---

# 一、上輪戰果：資訊沒有消失，但轉換可能很貴

第三輪已經排除一條過度簡單的資訊論論證：

$$
2^n\text{ 個候選}
\not\Rightarrow
2^n\text{ 位元資訊必須被保存}.
$$

SAT 的輸入長度只有 $n$，判定輸出甚至只有一位元。因此，不等號隊不能把「候選數量」直接等同於「資訊保存量」。

第三輪留下的研究物件是因果重建複雜度 CRC。其直覺為：

> 即使機器隨時能重新讀取全部輸入，它仍必須把分散在輸入中的約束關係重組成一個足以決定全域答案的結構。

因此第四輪提出：

$$
\boxed{
\text{CRC 的來源，是否就是局部資訊無法直接推出全域一致性的耦合？}
}
$$

不等號隊回答「很可能是」。

等號隊回答「小心，你又快把表示方式當成本體了」。

---

# 二、共同模型：局部約束與全域判定

令一個約束系統為：

$$
\Phi
=
\bigwedge_{i=1}^{m} C_i,
$$

其中每個約束 $C_i$ 只涉及少量變數。

局部演算法通常試圖從有限尺度的子系統推出全域資訊。例如，對某個整數 $k$，可以檢查所有大小不超過 $k$ 的局部區域是否相容。

為了避免將某一種 CSP 一致性算法直接當成一般模型，本輪只使用一個弱的語義概念：

## 2.1 $k$-局部可滿足性

定義：若任意至多 $k$ 個約束形成的子系統皆可滿足，則稱 $\Phi$ 為 $k$-局部可滿足：

$$
\operatorname{LSAT}_k(\Phi)=1.
$$

全域可滿足性則為：

$$
\operatorname{GSAT}(\Phi)
=
1
\iff
\exists x\;\Phi(x)=1.
$$

局部—全域落差可粗略記為：

$$
\operatorname{Gap}_k(\Phi)
=
\mathbf 1
\left[
\operatorname{LSAT}_k(\Phi)=1
\land
\operatorname{GSAT}(\Phi)=0
\right].
$$

若對很大的 $k$ 仍有：

$$
\operatorname{Gap}_k(\Phi)=1,
$$

就代表單靠有限尺度局部檢查無法發現全域矛盾。

但本輪要驗證的正是：

$$
\boxed{
\operatorname{Gap}_k\text{ 很大}
\stackrel{?}{\Longrightarrow}
\text{一般計算困難}.
}
$$

---

# 三、不等號隊出牌：全域耦合核心

不等號隊提出直覺：

> 若所有局部片段都可相容，矛盾只有在大量區域被同時耦合後才出現，那麼任何精確求解器似乎都必須完成某種全域重建。

令約束交互圖或超圖為：

$$
H_\Phi=(V,E),
$$

其中變數為頂點，約束形成邊或超邊。

若局部子圖都無法判斷全域答案，則不等號隊希望存在某種耦合量：

$$
\Gamma_{\mathrm{global}}(\Phi),
$$

使：

$$
\Gamma_{\mathrm{global}}(\Phi)\uparrow
\Rightarrow
\operatorname{CRC}(\Phi)\uparrow.
$$

第一個自然候選包括：

- 圖寬／樹寬；
- 約束超圖的展開性；
- 最小分隔集；
- 局部一致性階數；
- 消去寬度；
- 證明寬度；
- 跨區域殘餘類數。

如果這些量同時很大，是否就代表沒有簡單全域摘要？

此時 Tseitin 公式登場。

---

# 四、核心思維實驗：Tseitin 的局部—全域陷阱

令：

$$
G=(V,E)
$$

為連通無向圖。對每條邊 $e\in E$ 放置布林變數：

$$
x_e\in\{0,1\}.
$$

對每個頂點 $v$ 指定 charge：

$$
\chi(v)\in\{0,1\}.
$$

每個頂點要求其相鄰邊變數滿足奇偶約束：

$$
\bigoplus_{e\ni v}x_e
=
\chi(v).
$$

完整系統為：

$$
T(G,\chi)
=
\bigwedge_{v\in V}
\left(
\bigoplus_{e\ni v}x_e=\chi(v)
\right).
$$

## 4.1 全域矛盾

將所有頂點方程在 $\mathbb F_2$ 上相加。

每條邊恰好連接兩個端點，所以每個 $x_e$ 在左側出現兩次：

$$
x_e+x_e=0\pmod 2.
$$

因此左側總和為：

$$
0.
$$

右側則為：

$$
\bigoplus_{v\in V}\chi(v).
$$

若總 charge 為奇數：

$$
\bigoplus_{v\in V}\chi(v)=1,
$$

便得到：

$$
\boxed{0=1}.
$$

所以完整系統不可滿足。

## 4.2 幾乎完美的局部一致性

另一方面，對連通圖，任選一個頂點 $v$，都可以選擇邊賦值滿足其他所有頂點的奇偶約束，只讓矛盾集中到 $v$。

因此：

$$
\forall v\in V,
\quad
T(G,\chi)\setminus C_v
\text{ 可滿足}.
$$

進一步，任何真子集的頂點約束都至少漏掉某一個頂點，因此也可被上述某個賦值滿足。

也就是：

$$
\boxed{
\text{每個真子系統都可滿足，但整體不可滿足。}
}
$$

這幾乎是局部—全域落差的理想玩具模型。

不等號隊歡呼：抓到了！

---

# 五、不等號隊加碼：在某些證明系統裡，它真的很難

Tseitin CNF 在展開圖上是證明複雜度中的典型困難族。

對 resolution、regular resolution 與若干受限證明系統，已知 Tseitin 公式的證明大小、寬度、空間等資源會受到圖展開性、樹寬等結構參數控制，並可得到指數或近指數下界。

這給不等號隊一個非常誘人的故事：

$$
\text{局部約束}
\rightarrow
\text{高耦合圖}
\rightarrow
\text{局部推理難以整合}
\rightarrow
\text{指數證明}.
$$

因此提出候選命題：

> **局部—全域耦合猜想（第一版）**  
> 若一個不可滿足約束族具有高階局部可滿足性，且其交互圖不存在低寬度分解，則任何精確求解程序都必須付出超多項式的全域整合成本。

如果成立，它將把第三輪 CRC 具體化：

$$
\operatorname{CRC}(\Phi)
\approx
\text{局部資訊整合成全域矛盾的最低成本}.
$$

然後等號隊開始笑了。

---

# 六、等號隊反殺：你們忘了高斯消去

Tseitin 約束本身不是任意布林約束，而是：

$$
\boxed{
\mathbb F_2\text{ 上的線性方程組。}
}
$$

把系統寫成矩陣：

$$
Ax=b\pmod 2.
$$

則可直接使用高斯消去判斷：

$$
\operatorname{rank}(A)
\stackrel{?}{=}
\operatorname{rank}([A\mid b]).
$$

若秩不同，系統不可滿足。

整個運算為多項式時間。

更糟的是，在 Tseitin 的奇數 charge 情形，甚至不需要完整高斯消去；把所有方程加總便立刻得到：

$$
0=1.
$$

因此：

$$
\boxed{
\text{強烈的局部—全域落差}
\not\Rightarrow
\text{一般計算困難}.
}
$$

同一個數學對象，在 CNF + resolution 表示中可能需要極長局部推導；但切換到 XOR／線性代數表示後，全域耦合被一個代數不變量直接壓縮。

這正是本系列起點影片的高階版本：

$$
\text{很多局部條件判斷}
\rightarrow
\text{一個數學結構}
\rightarrow
\text{直接求值}.
$$

剪刀石頭布是三個狀態的玩具案例；Tseitin 則展示：即使局部—全域結構極其強烈，只要存在適當數學座標系，整體仍可能被多項式壓縮。

---

# 七、本輪第一個重大淘汰

以下命題正式淘汰：

$$
\boxed{
\text{局部都可滿足而全域不可滿足}
\Rightarrow
\text{問題一般性困難}.
}
$$

不成立。

同樣，下列敘述也不夠：

$$
\text{高樹寬}
\Rightarrow
P\neq NP,
$$

$$
\text{高展開性}
\Rightarrow
P\neq NP,
$$

$$
\text{resolution 指數下界}
\Rightarrow
P\neq NP.
$$

這些都可能只代表：

$$
\boxed{
\text{某種表示／推理語言無法有效看到真正的全域結構。}
}
$$

換句話說，一個「困難性證明」本身，也可能只是另一種座標系選錯了。

---

# 八、等號隊的核心哲學：找對座標系，就可能沒有搜索

等號隊把影片啟發正式提升為：

## 8.1 表示坍縮原理（等號隊候選）

對某些看似需要大量局部判斷的問題，存在一個轉換：

$$
\tau:
\Phi
\mapsto
R(\Phi),
$$

使：

$$
|R(\Phi)|\leq\operatorname{poly}(|\Phi|),
$$

$$
T_\tau(\Phi)\leq\operatorname{poly}(|\Phi|),
$$

且全域答案可由一個短求值：

$$
\operatorname{Eval}(R(\Phi))
$$

在多項式時間得到。

對 parity 系統：

$$
\tau
=
\text{轉為 }\mathbb F_2\text{ 線性代數}.
$$

這說明：

$$
\text{搜索困難}
$$

可能不是問題的本體，而只是表示的副作用。

等號隊因此提出更強的 $P=NP$ 預演：

> 也許 SAT 中尚存在一個未知的全域數學表示，就像 XOR-SAT 對應線性代數、2-SAT 對應蘊含圖、Horn-SAT 對應前向推導；一般 SAT 的「難」只是我們還沒找到對應的正規結構。

這仍不是證明，但它是一條完整且不能被「搜索空間很大」擊敗的立場。

---

# 九、不等號隊重新集結：真正要找的是表示抗性

不等號隊接受反殺並修改目標。

不再研究：

$$
\text{全域耦合是否存在}.
$$

而是研究：

$$
\boxed{
\text{全域耦合是否對所有有效表示都具有殘餘成本？}
}
$$

暫定命名：

$$
\boxed{
\text{Representation-Resistant Coupling Core}
\;(\mathrm{RRCC})
}
$$

中文：**表示抗性耦合核心**。

直覺上，若某實例族具有 RRCC，則：

1. CNF 局部推理不能壓縮；
2. 代數化後不能壓縮；
3. 圖分解不能壓縮；
4. 加輔助變數／擴維不能壓縮；
5. 精度或實數係數不能偷偷承載答案；
6. 預處理不能把指數成本藏到初始化；
7. 任一真正有效的全域摘要，都必須付出超多項式成本。

如果能嚴格證明這種對所有表示的抗性，確實將非常接近 $P\neq NP$。

然後等號隊立刻提醒：

> 你只要把「所有有效表示」寫進定義，就又把 $P\neq NP$ 藏回名稱裡了。

完全正確。

因此 RRCC **目前只能作為研究目標，不可作為已定義完成的不變量**。

---

# 十、避免循環：建立有限的「表示逃逸錦標賽」

既然不能直接量化所有可能表示，本系列採取實驗式方法。

建立一個可逐輪擴張的表示集合：

$$
\mathcal B_t
=
\{B_1,B_2,\ldots,B_t\},
$$

例如：

1. CNF + resolution；
2. branching program / BDD；
3. $\mathbb F_2$ 線性代數；
4. 一般多項式／Gröbner 類表示；
5. 樹分解／動態規劃；
6. cutting planes / LP；
7. semidefinite / SoS 類鬆弛；
8. extended formulations；
9. spectral / graph transform；
10. knowledge compilation；
11. 輔助變數與 extension systems；
12. 其他後續發現的有效表示。

對問題族 $F$ 與表示 $B$，定義實驗性成本：

$$
C(F;B).
$$

此處 $C$ 不要求是一個已證明的普適複雜度量，而是根據該表示最自然的資源：時間、空間、證明長度、寬度、degree、rank、表示大小等。

建立表示逃逸值：

$$
E_{\mathcal B_t}(F)
=
\min_{B\in\mathcal B_t} C(F;B).
$$

注意：

$$
E_{\mathcal B_t}
$$

**不是跨表示不變量，也不能證明 $P\neq NP$。**

它只是一個研究雷達：

- 若某問題族在某一欄突然變容易，表示它被該表示「逃逸」；
- 若一個問題族在越來越多彼此差異很大的表示中都保持困難，它就更值得研究其共同障礙；
- 若多種下界的數學證明反覆出現同一結構，就可能抽取更深候選不變量。

---

# 十一、第一張表示逃逸矩陣（概念版）

| 問題／實例族 | 局部 CNF 推理 | 線性代數 | 圖分解 | 擴展表示 | 暫定裁定 |
|---|---|---|---|---|---|
| Tseitin / parity | 可非常困難 | **多項式逃逸** | 視圖結構 | 依模型 | 淘汰為一般硬度證據 |
| 2-SAT | 易 | 非必要 | 蘊含圖多項式 | 易 | 已有結構坍縮 |
| Horn-SAT | 易 | 非核心 | 前向傳播 | 易 | 已有結構坍縮 |
| 一般 3-SAT | 未知一般多項式 | 無通用線性化 | 寬度大時 DP 昂貴 | 多模型未知 | 核心候選 |
| Pigeonhole 類 CNF | resolution 可困難 | 依編碼／域而異 | 依結構 | 某些強系統可縮短 | 表示敏感 |
| Clique / Coloring 編碼 | 多模型有下界 | 無已知通用坍縮 | 參數化可用 | 多面體下界存在 | 核心候選之一 |

此表刻意不填「已證明一般困難」，因為我們目前沒有這種證明。

---

# 十二、局部一致性理論給出的另一個提醒

約束滿足問題中確實存在一整類模板，可以由有界寬度的局部一致性方法解決；但也存在需用不同代數工具處理的可解類別，例如線性方程模二。

因此即使在已充分分類的 CSP 子世界中，也已經看到：

$$
\boxed{
\text{「可解」本身可能來自完全不同的結構機制。}
}
$$

有些問題因局部一致性足夠而容易；

有些問題因代數閉包而容易；

有些問題因圖結構有界而容易；

有些問題可能依賴尚未發現的結構。

這使 $P=NP$ 方的「未知表示革命」不能被輕易排除，也使 $P\neq NP$ 方必須尋找比單一算法範式更深的障礙。

---

# 十三、第四輪雙方正式攻防

## 13.1 不等號隊

### 主張 A：局部—全域落差是真現象

Tseitin 等公式證明：

$$
\text{大量局部一致}
\land
\text{全域矛盾}
$$

完全可能同時成立。

所以全域重建不是虛構問題。

### 主張 B：某些表示確實遭遇指數下界

解析證明、regular resolution、有限深度系統等已顯示：不同受限推理架構在高耦合實例上會真正爆炸。

### 主張 C：多種下界也許只是同一深層障礙的投影

若 resolution width、treewidth、communication cut、extension complexity 等在不同模型中反覆指向某種「跨區域依賴無法被局部壓縮」現象，可能存在尚未形式化的共同核心。

## 13.2 等號隊

### 反擊 A：Tseitin 本身就是你們的反例

你們最漂亮的局部—全域困難案例，恰好被 $\mathbb F_2$ 線性代數多項式解掉。

### 反擊 B：多種下界共同出現，仍不代表不存在另一個座標系

即使十種已知表示都困難，第十一種未知表示仍可能把結構壓縮。

### 反擊 C：真正的 $P=NP$ 算法不需要「模擬搜索」

就像高斯消去不需要模擬 resolution 一樣，一個一般 SAT 的多項式算法可能根本不在現有證明系統的幾何中活動。

### 反擊 D：如果你量化所有可能表示，你只是重述原問題

所以不等號隊必須找到一個由基本數學性質推出、而不是由「所有算法都做不到」定義出來的量。

---

# 十四、本輪與影片中介層的重新連接

最初影片展示：

$$
\text{條件規則}
\rightarrow
\text{數學函數}
\rightarrow
\text{狀態機執行}.
$$

本輪 Tseitin 案例展示同一思想的高階形式：

$$
\text{大量局部 parity 約束}
\rightarrow
\text{線性方程組}
\rightarrow
\text{全域代數消去}.
$$

因此中介層現在獲得一個新的重要作用：

$$
\boxed{
\text{形式化與數學構造不只是把答案實作，還能徹底改變計算路徑。}
}
$$

同一問題在不同數學構造下，可出現：

$$
\text{長局部推導}
$$

與：

$$
\text{短全域求值}
$$

之間的巨大差異。

所以要證明 $P\neq NP$，真正需要排除的不是「所有搜索技巧」，而是：

$$
\boxed{
\text{所有可能的多項式可建構數學重表示。}
}
$$

這正是難點所在。

---

# 十五、障礙審查

## 15.1 相對化

若「局部—全域耦合」論證只把子問題當黑箱，容易落入相對化框架。

**狀態：** 尚未通過。

## 15.2 自然證明

若我們找到一個可有效辨識、對大多數函數都很大的結構量，再用它排除小電路，需立即檢查自然證明障礙。

**狀態：** 高風險。

## 15.3 代數化

本輪反而顯示代數化可能是等號隊的逃逸工具。若不等號隊未來使用代數不變量做下界，仍需檢查 algebrization。

**狀態：** 雙刃劍。

## 15.4 證明系統依賴

Tseitin 在某證明系統困難、在另一代數系統容易，直接證明：

$$
\text{proof-system lower bound}
\neq
\text{general algorithm lower bound}.
$$

**狀態：** 本輪已形成明確反例。

---

# 十六、本輪淘汰的錯誤路線

以下論證不得直接用來推出 $P\neq NP$：

1. 每個小局部都可滿足，但整體不可滿足，所以一定很難；
2. 約束圖具有高樹寬，所以所有算法都必須指數時間；
3. 某一局部推理系統需要指數證明，所以不存在其他多項式算法；
4. 需要「全域資訊」所以一定需要遍歷整個組合空間；
5. 找到很多不同模型的下界後，未證明共同機制便直接相乘成守恆律；
6. 定義「對所有表示都困難」後，把這個定義本身當成新定理。

---

# 十七、本輪暫定成果

## 17.1 成果一：局部—全域落差是真實但不足

局部一致性與全域真值確實可嚴重分離。

但：

$$
\boxed{
\text{局部—全域落差}
\not\Rightarrow
\text{一般計算下界}.
}
$$

## 17.2 成果二：Tseitin 成為雙方共用教材

對不等號隊，它展示全域耦合與受限證明系統下界。

對等號隊，它展示數學重表示可以徹底消除原推理語言中的困難。

因此它是本系列目前最漂亮的雙面案例。

## 17.3 成果三：CRC 必須加入「最佳表示」問題

第三輪的因果重建複雜度不能只相對於原始表示。

更合理的研究形式是：

$$
\operatorname{CRC}(\Phi\mid B),
$$

即相對某數學基底 $B$ 的重建成本。

若要走向一般下界，就會自然詢問：

$$
\inf_B
\operatorname{CRC}(\Phi\mid B).
$$

但若 $B$ 量化所有可能有效算法，這就會循環回原始 $P/NP$。

因此現階段只能做可擴展的有限表示錦標賽。

## 17.4 成果四：提出表示抗性耦合核心 RRCC 作為遠期目標

RRCC 不是已完成定義，而是研究方向：

> 是否存在某種基本數學結構，能證明一個問題族的全域耦合無法被任何多項式可建構重表示消去？

這會成為後續幾輪的長期主線之一。

---

# 十八、第四輪比分

本輪不等號隊先靠 Tseitin 的局部—全域落差與 resolution 下界得分；等號隊隨後用 $\mathbb F_2$ 高斯消去漂亮反殺。

因此：

$$
P=NP:3
$$

$$
P\neq NP:3.
$$

比分純屬研究遊戲介面。

數學上目前仍為：

$$
\boxed{\text{未決}.}
$$

---

# 十九、第五輪入口：表示逃逸錦標賽

下一輪不再只抽象談「可能還有其他表示」。

我們要真的建立：

$$
\boxed{
\text{Representation Escape Matrix}
}
$$

選取多個經典困難族：

- Tseitin；
- Pigeonhole；
- 隨機 3-SAT／結構化 3-SAT；
- Clique；
- Graph Coloring；
- Subset Sum 類；
- 其他適合的 NP-complete 編碼。

再用多種表示與證明語言逐欄攻擊：

$$
\text{邏輯}
\leftrightarrow
\text{代數}
\leftrightarrow
\text{圖結構}
\leftrightarrow
\text{幾何／凸化}
\leftrightarrow
\text{知識編譯}
\leftrightarrow
\text{擴展變數}.
$$

目的不是用「很多模型都失敗」冒充證明，而是尋找：

$$
\boxed{
\text{不同失敗證明中反覆出現的共同數學結構。}
}
$$

若存在，它才可能成為真正跨表示不變量的種子。

---

# 二十、歷史依賴

1. `00_數學構造狀態機中介層_v1.0.md`
   - 提供「語義規則 → 數學構造 → 基底狀態機」轉換鏈。
2. `01_第一輪_存在量詞狀態坍縮.md`
   - 建立存在量詞壓縮器 $\mathcal C_{\exists}$。
3. `02_第二輪_跨表示不變量爭奪戰.md`
   - 建立殘餘可分辨性與跨表示資格測試。
4. `03_第三輪_演算法軌跡切割與因果瓶頸.md`
   - 淘汰簡單資訊論，提出 CRC。
5. Neo.K 既有 P/NP 動態速率系列
   - 提供搜索、構造、執行、驗證、知識凝結與表示轉換背景。

---

# 二十一、外部理論參照

1. G. S. Tseitin，關於圖上奇偶約束與命題證明複雜度的經典構造。
2. E. Ben-Sasson and A. Wigderson, *Short Proofs Are Narrow—Resolution Made Simple*, JACM, 2001.
3. Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov, *Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs*, ECCC, 2019.
4. Nicola Galesi, Navid Talebanfard, Jacobo Torán, *Cops-Robber Games and the Resolution of Tseitin Formulas*, ECCC, 2018.
5. 關於 affine / XOR-CNF 公式的知識表示文獻：線性方程模二可用 Gaussian elimination 多項式時間求解與投影。
6. Schaefer 類 Boolean CSP 分類及後續 CSP bounded-width 理論：不同 tractable 類別可由不同結構機制求解。

---

## 本輪裁定

$$
\boxed{
\text{「局部難、全域更難」不是答案；真正問題是全域結構能不能換座標系。}
}
$$

以及：

$$
\boxed{
\text{要證 }P\neq NP，必須找到連「表示革命」都無法逃逸的障礙。}
}
$$

這仍不是證明，但它把我們又從一條很像證明、其實會被代數表示擊穿的路線上救了回來。