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

## 共同保存結構崩塌與動態橋接：局部可解之間的介面，是否重新生成存在量詞？

**Round 11: Collapse of Common Preservation Structure and Dynamic Bridging**

- **主導研究者：** Neo.K（許筌崴）
- **協作整理：** Aletheia
- **機構：** EveMissLab（一言諾科技有限公司）
- **日期：** 2026 年 8 月 1 日
- **版本：** v1.0
- **研究狀態：** 第十一輪雙假設預演
- **前置文件：** `10_第十輪_多重反結構核心與異質黏合債務.md`
- **遊戲態度：** 等號隊與不等號隊互相拆橋
- **文件標準：** 遊戲比分不代表數學證據；所有一般化結論均需額外證明

---

## 摘要

第十輪將研究焦點由「某個問題缺乏哪種好結構」推進為「多種局部 tractable 結構如何在全域黏合時失去共同低成本結構」，並提出 HGD（Heterogeneous Gluing Debt）與 Dynamic Algebra Switching。

本輪進一步形式化此衝突。設一個整體約束問題被分解為多個局部模組：

$$
F(B,Y_1,\ldots,Y_m)
=
\bigwedge_{i=1}^{m}F_i(B_i,Y_i),
$$

其中 $Y_i$ 為模組 $i$ 的私有變數，$B_i\subseteq B$ 為與其他模組共享的邊界變數。即使每個 $F_i$ 都屬於可多項式時間求解的局部理論，真正的全域問題仍可寫成：

$$
\exists B\;\bigwedge_{i=1}^{m}
\left[\exists Y_i\,F_i(B_i,Y_i)\right].
$$

因此可定義每個模組的**邊界延伸關係**：

$$
\mathcal E_i(B_i)
=
\left\{
 b_i\mid \exists Y_i\,F_i(b_i,Y_i)
\right\}.
$$

全域可滿足性便精確等價於：

$$
\exists b\in\{0,1\}^{B}
\quad
\forall i,
\quad
b|_{B_i}\in\mathcal E_i.
$$

這揭示本輪核心機制：**局部存在量詞可被各自消去，但全域存在量詞會在介面重新出現。** 本文稱此現象為「存在量詞再現」（Existential Reappearance）。

等號隊據此提出 Dynamic Algebra Switching 的加強版：局部模組不必共享同一 polymorphism 或同一代數，只要每個模組都有多項式時間 solver，且模組之間存在多項式大小、可組合、可精確協調的 boundary summary／bridge protocol，則全域仍可保持多項式時間。SMT、DPLL(T)、Nelson–Oppen theory combination，以及 2026 年出現的 CDCL(⊕) 類 SAT／XOR 深度整合，都提供了「不同推理代數可以由橋接層合作」的實際先例。

不等號隊則指出：bridge 本身可能成為新的組合核心。Nelson–Oppen 類方法需要讓局部 theory solvers 對 shared/interface variables 的 equality arrangement 達成一致；相關 theory-combination 文獻明確指出 arrangement 空間在最壞情況可能呈指數成本。更根本地，若 bridge framework 足以把任意 CNF 的每個 clause 都視為一個「局部容易模組」，並仍能以多項式成本協調所有共享變數，那該 bridge 本身就已經是一般 SAT solver。這形成新的「Bridge Universality Trap」。

本輪不宣稱得到 $P\neq NP$。其主要成果是把第十輪 HGD 轉成可精確展開的**介面協調問題**，並建立 Boundary Extension Relation、Existential Reappearance、Polynomial Bridge Principle 與 Bridge Universality Trap 四個工作物件。下一輪將研究：當 bridge language 不斷增強時，是否必然重新生成一個與原 SAT 等價的「介面 SAT」，以及 bridge 表達力、summary size 與 coordination cost 之間是否存在可獨立刻畫的階層。

---

# 一、本輪問題：局部都會算，為什麼合起來還可能難？

第十輪中，不等號隊嘗試利用 polymorphism intersection collapse：

$$
\operatorname{Pol}(\Gamma_1)
\cap\cdots\cap
\operatorname{Pol}(\Gamma_m)
$$

可能在異質 constraint families 黏合後失去足以支持已知 tractable algorithms 的共同運算。

等號隊的回答是：

> 我根本不需要全域只用一套代數。

例如：

- Horn 區塊使用 Horn propagation；
- XOR 區塊使用 $\mathbb F_2$ 線性代數；
- 2-SAT 區塊使用 implication graph；
- difference logic 使用 graph shortest-path／negative-cycle reasoning；
- arrays、EUF、linear arithmetic 使用各自 theory solver；
- 最外層由 SAT／SMT orchestration 決定何時切換。

這類系統在現代 SMT 中不是幻想。DPLL(T) 的基本精神就是將 propositional search 與 theory-specific decision procedures 合作；Nelson–Oppen theory combination 則研究如何把不同 theory solvers 在 shared variables 上組合成一個正確的總體 decision procedure。

所以不等號隊真正需要回答的已不是：

$$
\text{「為什麼不存在共同 polymorphism？」}
$$

而是：

$$
\boxed{
\text{「不同局部代數之間的橋接，是否本身必須承擔新的全域組合成本？」}
}
$$

---

# 二、共同模型：局部模組與邊界變數

令整體問題寫為：

$$
F
=
\bigwedge_{i=1}^{m}F_i(B_i,Y_i),
$$

滿足：

1. $Y_i$ 是模組 $i$ 的私有變數；
2. $Y_i\cap Y_j=\varnothing$，$i\neq j$；
3. $B_i$ 是模組 $i$ 與外部共享的介面變數；
4. $B=\bigcup_i B_i$。

假設每個局部模組 $F_i$ 都有自己的多項式時間決策程序：

$$
A_i\in P.
$$

但「局部可解」真正提供的是：若給定邊界值 $b_i$，我們能判斷是否存在私有變數延伸：

$$
\operatorname{Ext}_i(b_i)
=
1
\iff
\exists Y_i\,F_i(b_i,Y_i).
$$

定義：

$$
\boxed{
\mathcal E_i
=
\{b_i:\operatorname{Ext}_i(b_i)=1\}
}
$$

為模組 $i$ 的 **Boundary Extension Relation（BER，邊界延伸關係）**。

此定義故意只記錄「哪些介面狀態可以向模組內部延伸」，不保留局部求解的全部歷史。

---

# 三、存在量詞再現引理

若私有變數 $Y_i$ 彼此不重疊，則：

$$
\exists B,Y_1,\ldots,Y_m
\bigwedge_{i=1}^{m}F_i(B_i,Y_i)
$$

等價於：

$$
\exists B
\bigwedge_{i=1}^{m}
\left(\exists Y_iF_i(B_i,Y_i)\right).
$$

利用 BER，可再寫成：

$$
\boxed{
\exists B
\bigwedge_{i=1}^{m}
\left[B_i\in\mathcal E_i\right].
}
$$

這裡沒有任何複雜度結論，只是一個量詞與私有變數分離後的邏輯等價。

但它揭示一個重要結構：

$$
\text{local solving}
\longrightarrow
\text{boundary projection}
\longrightarrow
\text{global coordination}.
$$

局部 solver 可以各自消去：

$$
\exists Y_i,
$$

但全域仍留下：

$$
\exists B.
$$

本文稱此現象為：

$$
\boxed{
\text{Existential Reappearance／存在量詞再現}
}
$$

即：

> 將一個全域存在問題拆成多個 tractable modules，並不會自動消除存在性；存在量詞可能只是從模組內部被推到模組介面。

---

# 四、第一個反例：每個 clause 都超級容易

考慮任意 CNF：

$$
F=C_1\land C_2\land\cdots\land C_m.
$$

若把每一個 clause $C_i$ 當成獨立模組，那麼每個局部問題都極其容易：

$$
C_i
$$

只要不是空 clause，單獨都很容易判斷、也很容易找滿足賦值。

所以：

$$
\forall i,
\quad
A_i\in P.
$$

甚至可以說局部 cost 幾乎是常數級。

但所有 clause 共享同一批變數，而全域條件是：

$$
\exists x_1,\ldots,x_n
\quad
\bigwedge_i C_i(x).
$$

也就是原本的 SAT。

因此：

$$
\boxed{
\text{「所有模組都在 P」本身幾乎沒有全域複雜度含義。}
}
$$

如果 bridge 可以任意把 clause-level local solvers 多項式地協調起來，那 bridge 已經解了 SAT。

這就是本輪第一個重要警告：

$$
\text{local tractability}
\neq
\text{compositional tractability}.
$$

---

# 五、等號隊出牌：Polynomial Bridge Principle

等號隊接受 bridge 不是免費的，但提出一個明確的充分條件。

對每個模組 $F_i$，假設存在一個 boundary compiler：

$$
\operatorname{Comp}_i(F_i)
\mapsto
S_i,
$$

其中 $S_i$ 是 BER $\mathcal E_i$ 的精確摘要，且滿足：

$$
|S_i|\leq\operatorname{poly}(|F|),
$$

$$
T_{\operatorname{Comp}_i}\leq\operatorname{poly}(|F|).
$$

再假設存在 bridge algorithm：

$$
\operatorname{Bridge}(S_1,\ldots,S_m)
$$

能在多項式時間判斷是否存在共同邊界：

$$
\exists b
\quad
\forall i,
\quad
b|_{B_i}\in\mathcal E_i.
$$

則整體問題顯然可在多項式時間解決。

因此得到一個有限模型內的充分原理：

## Polynomial Bridge Principle（PBP）

若：

1. 模組數量為多項式；
2. 每個局部模組可多項式求解；
3. 每個 boundary relation 可多項式時間編譯成多項式大小精確摘要；
4. 摘要間的 compatibility／join 可多項式時間判定；
5. witness lifting 亦為多項式；

則整體問題屬於 $P$。

這不是新的深定理，而是一個成本帳本：它清楚說明 Dynamic Algebra Switching 真正需要哪些 bridge 條件。

---

# 六、SMT／Theory Combination：動態橋接真的存在

等號隊現在可以拿成熟的 automated reasoning 當實證案例。

## 6.1 Nelson–Oppen

Nelson–Oppen 的核心不是要求兩個 theories 共享同一套內部代數，而是在 signatures 適當分離、theories 滿足 stable infiniteness 等條件時，讓各自 decision procedures 對 shared variables 的 equality／disequality arrangements 達成一致。

簡化表示：

$$
T_1\text{-solver}
\quad\leftrightarrow\quad
\text{interface arrangement}
\quad\leftrightarrow\quad
T_2\text{-solver}.
$$

也就是：

$$
\text{不同局部代數}
+
\text{受控介面協調}
\Rightarrow
\text{可組合 decision procedure}.
$$

這直接支持 Dynamic Algebra Switching：

$$
\boxed{
\text{全域 tractability 並不要求所有局部模組共享同一 polymorphism。}
}
$$

## 6.2 DPLL(T)

DPLL(T) 再進一步把 Boolean SAT search 與 theory-specific solver 結合。SAT core 管理 propositional branching，theory solver 則負責檢查 theory consistency，並回傳 theory lemmas／conflicts。

這是一種真正的 orchestration：

$$
\text{Boolean reasoning}
\leftrightarrow
\text{theory reasoning}.
$$

## 6.3 CDCL(⊕)

2026 年 SAT Conference 的 CDCL(⊕) 工作則提供一個更貼近本系列的例子：經典 CDCL／Resolution 對 parity-heavy 問題可能很差，而將 parity equations 直接納入 proof language、unit propagation 與 conflict learning 後，可得到對 Res$(\oplus)$ 的對應，並在實驗中的 Tseitin 類問題上顯著改善。

這再次支持最初影片所帶來的命題：

$$
\text{換數學表示／推理原語}
$$

確實可能摧毀舊表示中的困難。

---

# 七、不等號隊反擊：Bridge Arrangement Explosion

Theory combination 同時提供不等號隊武器。

局部 solvers 必須對 shared variables 的關係達成一致。如果 shared variables 為：

$$
V=\{v_1,\ldots,v_k\},
$$

那麼一個完整 equality arrangement 本質上對 $V$ 建立 equivalence classes，並指定必要的 equality／disequality 關係。

可行 arrangement 的數量可隨 $k$ 快速成長；以所有 set partitions 計算，其數量由 Bell number $B_k$ 控制。

但本輪**不**從

$$
B_k\text{ 很大}
$$

直接推出：

$$
\text{theory combination 必須慢}.
$$

因為 convexity、equality propagation、care functions 與其他結構可能避免枚舉所有 arrangements。

真正可靠的結論只是：

> bridge 有自己的搜索空間，而高效組合需要額外結構來壓縮這個 interface search。

Jovanović–Barrett 的工作便直接指出，傳統 combination 方法的一個主要成本是 shared-variable arrangement guessing，並透過 equality propagation 與 care functions 減少真正需要關心的 pair。

所以：

$$
\boxed{
\text{橋接可以被壓縮，但「橋接壓縮本身」也需要結構。}
}
$$

---

# 八、Bridge Universality Trap

現在來到本輪最重要的自我拆台。

假設我們定義一個極強的 bridge framework $\mathfrak B$，它允許：

1. 任意數量的局部模組；
2. 每個模組只要 individually tractable 即可；
3. 任意 shared variables；
4. bridge 在多項式時間內決定所有模組是否有全域相容解。

那麼把任意 CNF：

$$
F=\bigwedge_iC_i
$$

的每個 clause 當成一個局部模組。

每個 clause 的局部判定都 trivial，但：

$$
\operatorname{Bridge}(C_1,\ldots,C_m)
$$

若能多項式決定 compatibility，就直接多項式解 SAT。

因此：

$$
\boxed{
\text{Universal Polynomial Bridge for arbitrary tractable local modules}
\Rightarrow
P=NP.
}
$$

這不是 $P=NP$ 的證明，而是說：

> 「局部容易 + 一個完全通用又免費的 bridge」本身已經是一個與 SAT solver 同等強的假設。

本文稱之為：

$$
\boxed{
\text{Bridge Universality Trap／橋接普適陷阱}
}
$$

它是第六輪 Closure Paradox 的 bridge 版本。

---

# 九、Existential Reappearance：存在量詞只是搬家

把前述結果重新寫成量詞形式：

$$
\exists B,Y_1,\ldots,Y_m
\bigwedge_iF_i(B_i,Y_i)
$$

局部 solver 可以處理：

$$
\exists Y_iF_i(B_i,Y_i),
$$

但最後仍需處理：

$$
\exists B.
$$

所以 Dynamic Algebra Switching 並沒有魔法消除存在量詞，而是嘗試建立一個低成本的表示：

$$
\exists B\;\Phi_{\mathrm{bridge}}(B).
$$

真正問題變成：

$$
\boxed{
\Phi_{\mathrm{bridge}}
\text{ 是否具有比原始 }F\text{ 更低成本的可解結構？}
}
$$

若有，等號隊成功。

若 bridge projection／join 重新生成一般 SAT 結構，不等號隊便把原困難追了回來。

因此本輪提出：

$$
\boxed{
\text{Existential Reappearance Principle}
}
$$

> 局部消去不保證全域消去；在模組化求解中，被局部消除的 existential search 可能以 boundary compatibility search 的形式重新出現。

目前它是結構原理，而不是複雜度下界定理。

---

# 十、Bridge Coordination Debt（BCD）

為延續第九輪 Quotient Debt 與第十輪 HGD，本文定義 bridge 的暫定資源帳本：

$$
\boxed{
\mathbf D_B
=
(
D_{\mathrm{project}},
D_{\mathrm{summary}},
D_{\mathrm{interface}},
D_{\mathrm{arrange}},
D_{\mathrm{propagate}},
D_{\mathrm{join}},
D_{\mathrm{lift}}
)
}
$$

其中：

- $D_{\mathrm{project}}$：將局部模組投影到 boundary relation 的成本；
- $D_{\mathrm{summary}}$：精確表示 BER 的大小／建構成本；
- $D_{\mathrm{interface}}$：介面變數與共享結構規模；
- $D_{\mathrm{arrange}}$：建立 equality／compatibility arrangements 的成本；
- $D_{\mathrm{propagate}}$：跨模組傳播資訊的成本；
- $D_{\mathrm{join}}$：尋找全域相容 boundary assignment 的成本；
- $D_{\mathrm{lift}}$：將 boundary solution 還原為完整 witness 的成本。

這裡不宣稱：

$$
\prod D_j
$$

或：

$$
\sum D_j
$$

具有任何守恆下界。

目前它只是研究帳本，用來防止等號隊把成本藏在「橋接」二字裡。

---

# 十一、兩種 bridge 成功模式

目前外部理論提供至少兩種清楚的 bridge 成功模式。

## 11.1 小介面／低寬度

若模組交互圖存在小 separator，則 boundary state 的可能性可以被小摘要管理。

這與 treewidth-based dynamic programming 的核心精神一致：

$$
\text{大問題}
\rightarrow
\text{小 separator state}
\rightarrow
\text{逐區塊 join}.
$$

## 11.2 強介面結構

即使 shared-variable 數量不小，如果 theory 具 convexity、stable infiniteness、politeness、強 equality propagation 等性質，也可能避免盲目枚舉全部 arrangements。

這一點在 Nelson–Oppen 與其後續 theory-combination 研究中有成熟例子。

所以真正的 bridge tractability 可能來自：

$$
\boxed{
\text{small interface}
\quad\text{或}\quad
\text{structured interface}
}
$$

而不是單純：

$$
\text{local modules are easy}.
$$

---

# 十二、等號隊升級：Dynamic Bridge Portfolio

等號隊拒絕只使用一種 bridge。

它提出：

$$
\boxed{
\text{Dynamic Bridge Portfolio（DBP）}
}
$$

可依介面特徵動態選擇：

$$
B_{\mathrm{eq}},
B_{\oplus},
B_{\mathrm{Horn}},
B_{\mathrm{graph}},
B_{\mathrm{sep}},
B_{\mathrm{SMT}},
B_{\mathrm{learn}},
\ldots
$$

例如：

- equality-heavy interface → congruence closure／Nelson–Oppen；
- XOR-heavy interface → Gaussian／CDCL$(\oplus)$；
- sparse graph interface → separator DP；
- propositional residual → CDCL；
- arithmetic interface → theory propagation；
- repeated conflicts → learned bridge constraints。

因此等號隊的新主張不是：

$$
\text{存在單一 universal algebra},
$$

而是：

$$
\boxed{
\text{存在 uniform polynomial orchestrator，能持續選擇與重構 bridge。}
}
$$

這是目前 $P=NP$ 方最接近「智能體／統籌者」角色的構造版本。

---

# 十三、不等號隊再攻：Bridge-of-Bridges Regress

不等號隊的回答是：

若系統要在多種 bridge 之間切換，就還需要一個更高層判斷：

$$
\text{現在應使用哪一個 bridge？}
$$

以及：

$$
\text{不同 bridge 產生的摘要是否相容？}
$$

因此可能形成：

$$
\text{local solvers}
\rightarrow
\text{bridges}
\rightarrow
\text{bridge orchestrator}.
$$

如果 orchestrator 本身也使用多個策略，還可能出現：

$$
\text{bridge-of-bridges}.
$$

但本輪再次警告：

不能僅從「層級可以一直加」推出超多項式下界。

真正需要證明的是：

> 是否存在一個 solver-independent 的結構，使任何有限層級的精確 bridge composition 都必須留下某個無法多項式壓縮的 compatibility problem？

目前沒有這個定理。

因此 Bridge-of-Bridges 只是一個下一步研究方向，不是證明。

---

# 十四、與前十輪的統一

目前研究線可以重新寫成：

$$
\text{Existential Search}
\rightarrow
\text{Representation}
\rightarrow
\text{Exact Quotient}
\rightarrow
\text{Local Algebra}
\rightarrow
\text{Heterogeneous Modules}
\rightarrow
\text{Boundary Relations}
\rightarrow
\text{Bridge Coordination}.
$$

前幾輪一直問：

$$
\text{候選能不能被商掉？}
$$

本輪則指出，即使局部候選已被成功商掉，仍可能需要：

$$
\boxed{
\text{商的商／摘要的協調}
}
$$

因此「複雜度轉移」現在至少出現三層：

$$
\text{search debt}
\rightarrow
\text{quotient debt}
\rightarrow
\text{bridge debt}.
$$

但仍沒有證明這三種 debt 的總和存在不可消失的超多項式下界。

---

# 十五、本輪雙方攻防裁定

## 15.1 等號隊得分

等號隊證明了一個重要概念錯誤：

$$
\text{缺乏共同 polymorphism}
\not\Rightarrow
\text{無法多項式組合}.
$$

Nelson–Oppen、DPLL(T)、SMT 與 CDCL$(\oplus)$ 都說明，不同 local reasoning systems 可以透過專門 bridge 合作。

## 15.2 不等號隊得分

不等號隊則把 HGD 成功形式化成 boundary coordination：

$$
\exists B
\bigwedge_i[B_i\in\mathcal E_i].
$$

也證明「所有 local modules 都在 P」不足以推出全域 P，因為 clause-level decomposition 可以讓所有局部問題 trivial，而 bridge 仍完全承擔 SAT。

因此本輪比分：

$$
P=NP:10
\qquad
P\neq NP:10.
$$

比分仍然只是遊戲介面。

---

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

以下論證不得直接使用：

1. 「不同 tractable classes 沒有共同 polymorphism，所以 $P\neq NP$。」
2. 「每個局部模組都在 P，所以整體也應在 P。」
3. 「shared-variable arrangements 很多，所以任何 combination 都必須枚舉全部。」
4. 「Nelson–Oppen 某版本最壞指數，所以一般 SAT 必然非多項式。」
5. 「多建一層 orchestrator 就必然更難。」
6. 「bridge cost 很高」若 bridge cost 被直接定義成最佳全域求解時間，會形成循環論證。
7. 以有限 bridge portfolio 失敗，直接推出不存在未知 bridge language。

---

# 十七、本輪正式成果

## 成果 A：Boundary Extension Relation

$$
\mathcal E_i(B_i)
=
\{b_i:\exists Y_iF_i(b_i,Y_i)\}
$$

提供了局部 solver 與全域 coordination 之間的精確中介層。

## 成果 B：Existential Reappearance

$$
\exists B,Y
\bigwedge_iF_i
\equiv
\exists B
\bigwedge_i\exists Y_iF_i.
$$

局部量詞消去後，全域 existential search 可在介面再現。

## 成果 C：Polynomial Bridge Principle

局部 tractability 只有在 boundary summary 與 bridge join 同時可多項式處理時，才組合成全域 tractability。

## 成果 D：Bridge Universality Trap

若 bridge framework 能無條件、多項式地組合任意 tractable local constraints，則 clause decomposition 使其直接成為一般 SAT solver。

## 成果 E：Bridge Coordination Debt

建立：

$$
\mathbf D_B
$$

作為後續追蹤 projection、summary、interface、arrangement、propagation、join、lifting 的統一帳本。

---

# 十八、第十二輪入口：Bridge Language Hierarchy

本輪留下的真正問題是：

$$
\boxed{
\text{bridge 到底可以多有表達力，而又不重新變成一般 SAT？}
}
$$

第十二輪暫定題目：

## 介面語言階層與遞迴 SAT：橋越強，是否越接近把原問題重新生成？

準備建立 bridge language hierarchy：

$$
\mathcal B_0
\subseteq
\mathcal B_1
\subseteq
\cdots
\subseteq
\mathcal B_k
\subseteq\cdots
$$

例如：

- $\mathcal B_0$：單純 equality／disequality；
- $\mathcal B_1$：implication／2-SAT relations；
- $\mathcal B_2$：affine／XOR relations；
- $\mathcal B_3$：Horn／bounded-width summaries；
- $\mathcal B_4$：knowledge-compiled boundary circuits；
- 更高階：混合／可學習 bridge relations。

核心爭議：

$$
\text{bridge expressiveness}\uparrow
$$

是否伴隨：

$$
\text{bridge coordination complexity}\uparrow,
$$

以及是否存在一個非循環的臨界點：

$$
\boxed{
\text{一旦 bridge 足以無損表示一般 SAT 的邊界關係，橋本身就重新成為 SAT。}
}
$$

---

# 十九、歷史依賴

本輪直接依賴：

1. `07_第七輪_代數不變量爭奪戰與演算法代數橋.md`
2. `08_第八輪_演算法代數橋壓力測試與精確商結構.md`
3. `09_第九輪_尋找SAT的Blossom與商化債務.md`
4. `10_第十輪_多重反結構核心與異質黏合債務.md`

概念依賴：

$$
\text{polymorphism}
\rightarrow
\text{exact quotient}
\rightarrow
\text{heterogeneous gluing}
\rightarrow
\text{boundary coordination}.
$$

---

# 二十、外部理論參照

1. Greg Nelson and Derek C. Oppen, **Simplification by Cooperating Decision Procedures**, 1979.
2. David Monniaux, **A Survey of Satisfiability Modulo Theory**, 2016.
3. Dejan Jovanović and Clark Barrett, **Being Careful about Theory Combination**, *Formal Methods in System Design*, 2013.
4. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, Cesare Tinelli, **Politeness and Stable Infiniteness: Stronger Together**, CADE 2021；及後續 2023 Journal of Automated Reasoning 版本。
5. Martin C. Cooper and Stanislav Živný, **Hybrid tractability of soft constraint problems**, 2010.
6. David A. Cohen, Martin C. Cooper, Páidí Creed, András Z. Salamon, **The tractability of CSP classes defined by forbidden patterns**, 2011.
7. **Extending CDCL to Disjunctions of Parity Equations**, SAT 2026；用於觀察 parity-aware bridge／proof language 如何改變 Tseitin 類問題上的推理行為。

---

## 本輪裁定

$$
\boxed{
\text{Dynamic Algebra Switching 是真的；但 Algebra Switching 的橋也必須被計算。}
}
$$

$$
\boxed{
\text{局部存在量詞消去，不等於全域存在量詞消失；它可能只是在 boundary 上再現。}
}
$$

目前最值得追的問題，不再是：

$$
\text{「有沒有共同代數？」}
$$

而是：

$$
\boxed{
\text{「不同代數的精確摘要，能否永遠用多項式成本協調？」}
}
$$

這將直接進入第十二輪。