基于SMT的不完全信息游戲求解①

李 健,鄭榮基,湯宇鋒,袁立然,陳 寅

(華南師范大學(xué) 計算機學(xué)院,廣州 510631)

1 概述

計算機博弈(也稱機器博弈)是人工智能領(lǐng)域的重要研究方向,是測試人工智能所達到水平的一個重要平臺.它以人工智能和各種計算機博弈技術(shù)為基礎(chǔ),研究如何讓計算機像人類一樣從事高度智能的博弈活動.根據(jù)掌握的信息完全程度不同,計算機博弈可分為完全信息博弈和非完全信息博弈[1].在完全信息博弈領(lǐng)域,已有較為成熟的人工智能技術(shù),最為出名的就是國際象棋領(lǐng)域的“深藍”以及圍棋領(lǐng)域的AlphaGo.而對于非完全信息博弈,由于博弈參與者掌握的信息有限,僅憑當(dāng)前有限的信息無法準(zhǔn)確推測對手所處的狀態(tài),更加難以準(zhǔn)確推斷與估計對手的決策行為,在研究上有相當(dāng)大的復(fù)雜性和不確定性.2017年1月,才由卡內(nèi)基梅隆大學(xué)研發(fā)的Libratus人工智能系統(tǒng)在德州撲克中戰(zhàn)勝人類玩家,之后鮮有其他人工智能系統(tǒng)攻克非完全信息博弈.

目前,整個非完全信息博弈的研究還處于初級階段.但是,在現(xiàn)實生活中大到國家,小到家庭,人們面臨的諸多問題都是以非完全信息的形式存在著.因此,非完全信息博弈的研究目的和意義所在,便是如何在已知的有限的信息的前提下,為人類的生活和發(fā)展提供指導(dǎo),以謀求最大的利益.現(xiàn)在,科技高速發(fā)展,移動互聯(lián)網(wǎng)發(fā)展更為迅猛,讓人工智能和計算機博弈的發(fā)展更加的多元化.人們的碎片化時間越來越多,閱讀、玩游戲等等成了人們娛樂消遣的主要方式.很多時候,玩家都是在和計算機博弈程序進行博弈[2].針對這一種現(xiàn)象,很多游戲產(chǎn)商將游戲中的人工智能放在業(yè)務(wù)重心之一.

“誰是殺手”是一種非完全信息的推理游戲,其要求玩家根據(jù)自己手中的牌以及游戲過程中所獲得的相關(guān)信息推理出殺手牌.本文以“誰是殺手”游戲為例,研究了一種基于SMT[3]的不完全信息游戲求解方法,旨在對非完備信息博弈進行學(xué)習(xí)與研究,同時設(shè)計并實現(xiàn)了一個能進行人機交互對戰(zhàn)的網(wǎng)頁平臺.

2 背景知識

2.1 游戲簡介

“誰是殺手”游戲(以下簡稱為“游戲”)是一種規(guī)則簡單同時又需要推理的卡牌游戲.游戲共有28張卡牌,分為四類,每類卡牌的編號為1至7.以下我們把類型為X(1≤X≤4)編號為Y(1≤Y≤7)的卡牌記為(X,Y).游戲可供3?5人玩,以下均以3人游戲為例.在游戲的準(zhǔn)備階段,每位玩家會隨機的分到9張牌,剩余的一張牌牌面向下放置在桌上,稱為“殺手牌”.游戲的目標(biāo)是玩家猜出這張殺手牌是什么.游戲開始后由每個玩家輪流進行行動,行動可以是以下A0～A2中的一種:

(1)A0玩家說出一張牌,如果它是殺手牌,則游戲結(jié)束.

(2)A1玩家向其它玩家請求卡牌和放置卡牌,具體來講分為以下3步:

1)A1.1玩家向其他兩位玩家請求某個類型的牌.

2)A1.2其他兩位玩家如果手中有這種類型的牌,則選取一張牌面向下交給當(dāng)前玩家;如果手中沒有這種類型的牌,則告訴所有玩家.

3)A1.3當(dāng)前玩家根據(jù)手中的牌,如果出現(xiàn)3張不同花色但是相同序號,或者3張相同花色并且連續(xù)序號的手牌時,需要將其中兩張暗置,只暴露其中一張來進行出牌;若手中沒有符合上述情形的三張手牌時,只需出手牌中的任意一張,無需暗置.

(3)A2玩家查閱一張.

這個游戲的一個重要的問題是,在每個回合玩家都需要判斷目前的信息是否已經(jīng)能夠斷定哪一張牌是殺手牌.實際上,在經(jīng)過若干回合后,即使能夠記住每個回合的動作,由人腦來推斷是否可以斷定殺手牌也是很困難的.例如,在A1.3中如果玩家放置了3張牌,其中暴露的牌是(2,3),按照規(guī)則玩家放置的3張牌可以是以下6中組合中的任意一種:

{(2,1),(2,2),(2,3)} {(2,2),(2,3),(2,4)} {(2,3),(2,4),(2,5)} {(1,3),(2,3),(3,3)} {(1,3),(3,3),(4,3)}{(2,3),(3,3),(4,3)}

例如,在A1.3中,如果玩家只放置了一張牌,能夠用于推理的信息則更加復(fù)雜.它表示玩家手中沒有任何類型的卡牌有3個連續(xù)的編號,同時也不存在某個編號的卡牌有3種類型.本文的工作就是使用邏輯工具來描述這個游戲的動態(tài)過程,并且以此為基礎(chǔ)來進行推理.

2.2 動態(tài)系統(tǒng)的邏輯描述

為了進行游戲的推理,首先需要能夠描述這個動態(tài)系統(tǒng).情景演算(situation calculus)是一種用來描述動態(tài)系統(tǒng)的邏輯語言[4].它在一階邏輯的基礎(chǔ)上增加了狀態(tài)和動作,因此可以用來描述在動作的作用下不斷變化的系統(tǒng).情景演算中主要有3類元素:情景(situation),動作(action)和實體流(fluent).實體流用來表示不同狀態(tài)下不同值的實體.

為了描述動態(tài)系統(tǒng),在情景演算中包含以下的幾類約束:

(1)初始狀態(tài)和約束,例如在游戲的開始,需要描述每張牌可能在某個玩家手里或者是殺手牌,以及每個玩家恰好持有9張牌.

(2)描述動作的前提和效果,例如某位玩家把一張牌放置在桌上的前提是這張牌這個回合在他手上,這個動作的效果是在下個回合牌的位置在桌上.

(3)描述持續(xù)性的約束,例如一張牌如果在前一個回合在某個玩家手上,那么如果沒有相關(guān)的動作,下個回合這張牌仍然應(yīng)該在這個玩家的手上.

游戲中,可以將每個玩家行動開始的時候狀態(tài)作為一個情景,描述這個情景下的卡牌的位置需要滿足的約束,以及玩家實際的動作所產(chǎn)生的約束等.為了更有效的實現(xiàn)系統(tǒng),我們直接使用命題邏輯的公式來描述了各種約束,以便隨后調(diào)用SMT[3]的求解器來求解.

2.3 SMT及其求解器

可滿足模理論(Satisfiability Modulo Theory,SMT)是判斷一階邏輯公式在組合背景理論下的可滿足性問題[3].SMT的背景理論使其能很好地描述實際領(lǐng)域中的各種問題,結(jié)合高效的可滿足性判定算法,SMT在測試用例自動生成、程序缺陷檢測驗證[5]、RTL (Register Transfer Level)驗證[6]、優(yōu)化問題求解[7,8]、靜態(tài)分析[9,10]、程序驗證[11,12]等一些最新研究領(lǐng)域中有著突出的優(yōu)勢.SMT求解技術(shù)的具體實現(xiàn)被稱為SMT求解器(SMT solvers).人們研發(fā)了很多SMT求解器,比較成熟的有Z3[13],CVC4[14],Yices2[15],MathSAT4[16],Boolector[17].其中,Z3是目前為止在擴展性、表達能力以及求解效率等方面都較為出色的SMT求解器.它不僅可以用來驗證多個邏輯公式的可滿足性,而且可以求出一組滿足約束的解.在本文中,我們使用2.2節(jié)所述方法編寫命題邏輯公式,調(diào)用Z3求解器來判斷公式的可滿足性.

3 推理的實現(xiàn)

假設(shè)玩家的數(shù)量為play_num,卡牌的類型為card_type,每類卡牌的數(shù)量為card_num,編號從1到card_num.類型為X編號為Y的卡牌記為(X,Y).

為了描述狀態(tài),需要以下的謂詞:

(1)turn(T,P):回合T的當(dāng)前玩家是玩家P.

(2)card(T,X,Y,S):卡牌(X,Y)在T回合的位置為S,其中,

1)T∈N,表示回合數(shù).

2)1≤P≤play_num,表示玩家P.

3)1≤X≤card_type,1≤Y≤card_num,表示類型為X編號為Y的卡牌.

4)0≤S≤play_num,S=0表示卡牌(X,Y)在桌上,否則表示卡牌在玩家S手中.

兩個描述動作的謂詞:

(3)move(T,X,Y,P):在回合T卡牌移動到了玩家P手中.

(4)put(T,X,Y):在回合T卡牌(X,Y)放到了桌上.

使用上述的描述狀態(tài)和動作的謂詞,我們可以精確的描述游戲的每個回合的動作和由此產(chǎn)生的狀態(tài)變化.由于本游戲是一個不完全信息游戲,因此在每個回合中,從不同的玩家視角看到的信息是不同.例如從玩家1的視角看,如果玩家2請求一張類型3的卡牌,那么玩家3交給玩家2的卡牌編號是未知的.

以下分別給出用來描述游戲中的動作的邏輯公式.由于玩家視角的不同,相同的動作由于獲得的信息不同,對應(yīng)的邏輯公式可能是不同的.

游戲開始記回合數(shù)t=0,如果玩家p分發(fā)到的卡牌為(x1,y1),…,(xn,yn)則增加公式:

確保所有的牌都發(fā)給了玩家,并且每個人都拿到了n張卡牌:

在每個回合的第一個階段是由當(dāng)前玩家向其他玩家請求一張線索牌.這里有3種情況:

(1)在回合t,玩家p1從玩家p2得到卡牌(x,y):

(2)在回合t,玩家p1從玩家p2得到類型x的卡牌,編號未知:

(3)在回合t,玩家p1從玩家p2請求類型x的卡牌,但是p2手中沒有類型x的卡牌:

在每個回合的第二階段是由當(dāng)前玩家放牌在桌上.這里有四種情況:

(1)在回合t,玩家p把3張牌(x1,y1),(x2,y2),(x3,y3)放在桌上:

(2)在回合t,玩家p把3張牌放在桌上,已知其中一張是(x,y),其余兩張未知:

(3)在回合t,玩家p把一張牌(x,y)放在桌上:

(4)在回合t,玩家p手中無牌,因此可以查看一張 桌面上的牌,假設(shè)是在回合t1放置在桌面上的牌(X,Y):

如果A={a1,…,an}是一個原子公式的集合,k∈N是一個自然數(shù),我們用AtMost(k,A)表示A中至多有k個公式為真,即如下的公式:

對于每個回合t,我們需要增加如下的公式來描述背景知識.

(1)回合t有1個當(dāng)前玩家

(2)在回合t至多有n張牌移動到來其它玩家手中

(3)在回合t至多有n張牌放置在桌上

(4)回合t結(jié)束時卡牌的位置

推理殺手牌的過程如算法1所示.定義一個SMT求解器Z3,將每回合產(chǎn)生的約束對應(yīng)的邏輯公式添加到Z3.在回合0,根據(jù)初始卡牌將式(1)和式(2)加入Z3.從回合1開始讀入數(shù)據(jù),并判斷在每個回合是否能夠確定殺手牌.如果Z3求解器返回SAT,說明有符合約束的解,如果將某一可能的殺手牌約束為非殺手牌后返回了UNSAT,說明該殺手牌是唯一可能的殺手牌,則返回該殺手牌,否則進行下一回合.

算法1.推理殺手牌的過程?1 Φ= ;2 t=0;// 回合0 3 根據(jù)初始卡牌將公式(1)和式(2)加入Φ;4 t=1;// 從回合1開始讀入數(shù)據(jù),并判斷再每個回5合是否能夠確定殺手牌6 while讀取回合t的信息do 7 根據(jù)回合t的動作,將公式(3)–(9)加入Φ;8 將回合t的背景知識公式(10)–(13)加入Φ;9 if check(Φ)=UNSAT then 10 返回錯誤;// 讀入數(shù)據(jù)有誤11 else 12 M是Φ的一個模型;13 (X,Y)是M中的殺手牌;// (X,Y)是可能14 的殺手牌15 if check(Φ∪?card(0,X,Y,0))=UNSAT then 16 return (X,Y)是殺手牌;// (X,Y)是唯一

17 可能的殺手牌18 t=t+1;// 進行下一回合

4 系統(tǒng)實現(xiàn)

本文除了解決“誰是殺手”游戲推理問題外,還對游戲進行了簡單實現(xiàn).玩家可以登錄網(wǎng)頁進行人機對戰(zhàn).系統(tǒng)包括客戶端和服務(wù)端兩部分,系統(tǒng)框架如圖1所示.游戲玩家在客戶端登陸,與服務(wù)端的AI玩家進行PK.

圖1 系統(tǒng)框架圖

4.1 客戶端

游戲玩家登陸網(wǎng)頁后,點擊“準(zhǔn)備”按鈕,客戶端進行初始化,并向服務(wù)端發(fā)送請求,服務(wù)端接收到后,模擬發(fā)牌操作,將手牌發(fā)給客戶端.當(dāng)客戶端接收后,解析并將收到的手牌信息顯示給玩家.接著玩家可以根據(jù)游戲狀態(tài)點擊“問牌”、“看牌”、“出牌”、“給牌”、“猜牌”按鈕進行相應(yīng)操作.服務(wù)端接收到客戶端動作消息后模擬AI用戶做出應(yīng)答操作.

4.2 服務(wù)端

在服務(wù)端中,不僅要響應(yīng)客戶端的請求,還要模擬AI玩家游戲過程,進行“猜牌”、“問牌”、“給牌”、“出牌”、“看牌”這些操作.當(dāng)輪到AI玩家給牌時,判斷是否持有符合要求的卡牌,有則打出卡牌;當(dāng)輪到AI玩家看牌時,隨機選擇某個回合放置在桌面的未知卡牌進行查看;當(dāng)輪到AI玩家出牌時,隨機打出符合要求的卡牌;當(dāng)輪到AI玩家問牌時,隨機選擇一張未知卡牌.服務(wù)端會以AI玩家的視角,記錄游戲過程.AI玩家的推理過程如算法1所示.

5 總結(jié)與展望

本文提出了一種基于SMT的不完全信息游戲求解方法并基于此方法實現(xiàn)了一個“誰是殺手”游戲應(yīng)用,該應(yīng)用提供了一個能進行人機交互對戰(zhàn)的網(wǎng)頁平臺.游戲用戶在客戶端登陸便可與服務(wù)器端的AI進行游戲?qū)?zhàn).AI玩家能夠應(yīng)用Z3求解器推理出殺手牌,但在問牌和出牌游戲動作時,沒有添加任何優(yōu)化策略,只是能夠打出符合規(guī)則的手牌,不會去考慮游戲的利益關(guān)系,處于一種“初級”玩家的智能水平.因此,下一步研究內(nèi)容是通過優(yōu)化AI玩家問牌和出牌策略,使“出牌”的次數(shù)盡量少,同時獲得的線索信息盡可能更多,從而加強AI玩家的智能程度,加快推理過程.