# P3全部八子集求minimum cover [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-minimum-vertex-cover/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-minimum-vertex-cover-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 完整分類所有covers與全部minimizers。 bounded finite exact enumeration，不使用König theorem。 ## 已知條件與符號 - work - G1 — V={0,1,2}，E={01,12}。 - V,E — 完整頂點與邊集合 - τ(G) — minimum cover基數 ## 規則與來源 本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。 - mko_definition · cited — 對bounded finite simple undirected graph完整枚舉全部vertex subsets，逐一做all-edge cover audit，得到minimum cardinality與全部minimizers。給定nonminimum cover時須明示更小cover witness；inclusion-minimal只表示刪任一點即失去cover，不等於minimum。empty graph、multiple minima與minimal-but-not-minimum均保留。不得混同maximal、edge cover、independent set，也不使用König theorem或weighted/directed variants。 · mko-minimum-vertex-cover - work · prerequisite — 有限無向簡單圖的邊為無loop、無重複unordered pairs；圖性質須對完整明示V、E逐一檢查。 cover必與每條邊有共同端點；minimum基數在全部合法covers中最小，argmin列出全部達此值的covers；minimal只禁止刪選點。 ## 逐步主鏈 S01 · implies操作前 |V|=3 操作後 2^3=8\text{ vertex subsets} 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 每頂點選或不選，完整候選八個。 S02 · implies操作前 C=\varnothing 操作後 01\cap C=\varnothing\implies\text{invalid} 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 空集合沒有覆蓋原邊01。 S03 · implies操作前 C=\{0\},\quad C=\{2\} 操作後 12\text{ uncovered},\quad01\text{ uncovered} 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 兩個端點singleton各給明確失敗邊。 S04 · implies操作前 C=\{1\} 操作後 01\cap C=12\cap C=\{1\}\implies\text{valid, size }1 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 中心singleton覆蓋兩邊。 S05 · implies操作前 C=\{0,1\},\quad C=\{1,2\} 操作後 \text{both cover }01,12\text{ via vertex }1 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 含中心的兩個二點子集皆cover。 S06 · implies操作前 C=\{0,2\} 操作後 01\text{ covered by }0,\quad12\text{ by }2 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 不含中心的二點集也cover，且刪任一點就失敗。 S07 · implies操作前 C=\{0,1,2\} 操作後 \text{cover, size }3 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 最後triple覆蓋兩邊，八候選全部完成。 S08 · implies操作前 \text{valid sizes }1,2,2,2,3 操作後 \tau(G)=1,\quad\operatorname{Argmin}=\{\{1\}\} 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 取所有合法covers最小基數並列全部minimizers。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — empty-edge graph則唯一size0 minimizer為空集；一般圖可能多minima。 - S07 · premise_audit · G1, S06, work — 有效covers為{1}、{0,1}、{0,2}、{1,2}、V。 - S06 · premise_audit · G1, S05, work — 故此集合minimal但不是minimum，因{1}更小。 - S05 · premise_audit · G1, S04, work — 它們刪掉端點仍cover，所以非minimal。 - S04 · premise_audit · G1, S03, work — 提供大小一上界但仍完成其餘分類。 - S03 · premise_audit · G1, S02, work — 兩案都保留。 - S02 · premise_audit · G1, S01, work — 圖有邊，所以空圖convention不適用。 - S01 · premise_audit · G1, work — 不是只測幾個可能最優候選。 ## 錯誤控制與反例 八案0點一案、1點三案、2點三案、3點一案。 全部argmin不只報大小1，還報唯一達標集合{1}。 - {0,2} minimum因刪任何點都失敗。 → reject — {1}是更小cover。 - {0}是cover。 → reject — 邊12未被覆蓋。 - minimum cover一定唯一。 → reject — 單邊圖的任一端點singleton都是minimum。 ## 結論與限制 minimum size1，唯一minimizer{1}；{0,2}為minimal但非minimum。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 0c5dcd41a728ed5ea6c8d3a9073f8c93e7136545d0106b2b4387bb0d79708b0c - original source SHA-256: 62c1c8fdcda2e9d32b26f78d86b566895ca1e88ad41eac54b7a4454148d6bafb - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-minimum-vertex-cover-01.json)