判斷 AOC 終局

基本上 RTS 都是 PSPACE-hard, 看這裏
不過今天打機時想到比較直接的 reduction, 也好像未看過類似的

判斷 AOC 終局
給出現時的遊戲情況, 判斷 player 1 能否勝出

True Quantified Boolean Formula
判斷一條這樣的 boolean formula 是否 true: ∃x₁∀x₂ ∃x₃∀x₄.....∃x_n-1∀x_n φ(x₁, x₂, x₃, x₄, ..., x_n-1, x_n)
可以假設條 formula 是 CNF

例如: ∃x ∀y ∃z ((x ∨ y) ∧ (y ∨ z) ∧ (¬y ∨ ¬z)) 是 true
因為可以 set x = T, 當 y = F 則 z = T, y = T 則 z = F

這個問題可以 reduce 為一個 2 player game:
- 順序 assign T/F 給每一個 variable
- player 1 負責 assign ∃ 的 variable
- player 2 負責 assign ∀ 的 variable

Assign 完後:
- player 2 選擇一個他認為沒有 satisfy 的 clause, 例如 (x₁ ∨ ¬x₅ ∨ x₈)
- player 1 選擇他認為這個 clause 其實是 true 的 variable, 例如 ¬x₅
- check 這個 variable 是否為之前的選擇, 即 test x₅ 是否選了 false, 是的話 player 1 勝出

假設雙方 play optimally, 如果 player 1 勝出即是 formula 為 true

AOC gameplay setup
Player 1 需要在限時內收集少量的木材, 否則 Player 2 勝出
具體做法是 player 2 有足夠多的兵力, 但被 player 1 的層層石牆圍著, 只要時間把石牆破壞便可以清場勝出
而 player 1 有接近無限肉和金, 但沒有木, 若可興建軍營便有足夠的兵力清場
而 player 1 能否成功收集少量的木便是勝出的關鍵

player 1 能否成功收集木材, 則取決於條 QBF 是否 true
遊戲流程與 player 1 村民的路徑:

如果 verify 成功, 則 player 1 的村民可以收集到木材
否則 player 1 只能等死

以下的圖中的 label:
藍色: player 1
紅色: player 2
淺藍: 海
淺綠: 陸地

Assumption:  player 1 的村民若試圖徒手破壞 player 2 的建築, 會花費太多時間而讓 player 2 勝出

Single use & directed road (P1/P2)
一方由左邊進入, 坐船到右邊
運輸船的 hp 剛好只能通過一次, 所以既不能往回走 / 到右邊接人到左邊

Player 1's choice (∃)
player1 的村民由左方進入, 炸藥筒的數量剛好足夠炸開其中一邊的石牆
炸開石牆除了可以繼續前進, 還要 assign 相應的的 T/F 給 x_i (後述)

Player 2's choice (∀)
如果沿用上述的 design, player 2 可以甚麼也不做, player 1 也無可奈何
所以要強制 player 2 作出選擇, 否則 player 1 可以任選一邊, 設計如下

player 2 可以做的是選擇一邊用塔封掉;
player 1 只能經沒有封掉的一邊通過並 assign 相應的的 T/F 給 x_i (後述)


Verify test
首先 player 2 choose clause 和 player 1 choose variable 用上面的 construction 可以構造
之前的 choose 和 verify 構造如下:



如果之前選擇了某 variable, 便可以在藍色圓圈處興建箭塔, 把 player 2 的遊俠射殺
這樣 player 1 的村民稍後在上方進入便可以安全伐木, 否則會被 player 2 的遊俠砍死

Planarization
按照原本的構造,  個 graph 可能不 planar
而 AOC 是 planar 的遊戲, 所以要做一做手腳
假設原本的路是左至右及下至上相交, 則改成:

如果 player 1 的村民由左方進入, 必需把左邊擋路的伐木場自爆掉才可繼續前進
在十字路口, 如果 player 1 選擇「正確」方向向右, 則 player 2 只可:
A) 開右邊的路, 讓 player 1 照目標前進
B) 開向下的路, player 1 就可以伐到木勝出

在十字路口, 如果 player 1 選擇「錯誤」方向向上, player 2 可以封掉向上的路
則 player 1 只能轉左, 雖然伐到樹, 但是原本的伐木場已經自爆掉, player 1 也 stuck 了

由於 TQBF 是 PSPACE-Complete, 由此得出判斷 AOC 終局是 PSPACE-Hard
參巧: 圍棋是 PSPACE-Complete 的 proof