李 健,鄭榮基,湯宇鋒,袁立然,陳 寅
(華南師范大學(xué) 計(jì)算機(jī)學(xué)院,廣州 510631)
計(jì)算機(jī)博弈(也稱機(jī)器博弈)是人工智能領(lǐng)域的重要研究方向,是測(cè)試人工智能所達(dá)到水平的一個(gè)重要平臺(tái).它以人工智能和各種計(jì)算機(jī)博弈技術(shù)為基礎(chǔ),研究如何讓計(jì)算機(jī)像人類一樣從事高度智能的博弈活動(dòng).根據(jù)掌握的信息完全程度不同,計(jì)算機(jī)博弈可分為完全信息博弈和非完全信息博弈[1].在完全信息博弈領(lǐng)域,已有較為成熟的人工智能技術(shù),最為出名的就是國(guó)際象棋領(lǐng)域的“深藍(lán)”以及圍棋領(lǐng)域的AlphaGo.而對(duì)于非完全信息博弈,由于博弈參與者掌握的信息有限,僅憑當(dāng)前有限的信息無法準(zhǔn)確推測(cè)對(duì)手所處的狀態(tài),更加難以準(zhǔn)確推斷與估計(jì)對(duì)手的決策行為,在研究上有相當(dāng)大的復(fù)雜性和不確定性.2017年1月,才由卡內(nèi)基梅隆大學(xué)研發(fā)的Libratus人工智能系統(tǒng)在德州撲克中戰(zhàn)勝人類玩家,之后鮮有其他人工智能系統(tǒng)攻克非完全信息博弈.
目前,整個(gè)非完全信息博弈的研究還處于初級(jí)階段.但是,在現(xiàn)實(shí)生活中大到國(guó)家,小到家庭,人們面臨的諸多問題都是以非完全信息的形式存在著.因此,非完全信息博弈的研究目的和意義所在,便是如何在已知的有限的信息的前提下,為人類的生活和發(fā)展提供指導(dǎo),以謀求最大的利益.現(xiàn)在,科技高速發(fā)展,移動(dòng)互聯(lián)網(wǎng)發(fā)展更為迅猛,讓人工智能和計(jì)算機(jī)博弈的發(fā)展更加的多元化.人們的碎片化時(shí)間越來越多,閱讀、玩游戲等等成了人們娛樂消遣的主要方式.很多時(shí)候,玩家都是在和計(jì)算機(jī)博弈程序進(jìn)行博弈[2].針對(duì)這一種現(xiàn)象,很多游戲產(chǎn)商將游戲中的人工智能放在業(yè)務(wù)重心之一.
“誰是殺手”是一種非完全信息的推理游戲,其要求玩家根據(jù)自己手中的牌以及游戲過程中所獲得的相關(guān)信息推理出殺手牌.本文以“誰是殺手”游戲?yàn)槔?研究了一種基于SMT[3]的不完全信息游戲求解方法,旨在對(duì)非完備信息博弈進(jìn)行學(xué)習(xí)與研究,同時(shí)設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)能進(jìn)行人機(jī)交互對(duì)戰(zhàn)的網(wǎng)頁(yè)平臺(tái).
“誰是殺手”游戲(以下簡(jiǎn)稱為“游戲”)是一種規(guī)則簡(jiǎn)單同時(shí)又需要推理的卡牌游戲.游戲共有28張卡牌,分為四類,每類卡牌的編號(hào)為1至7.以下我們把類型為X(1≤X≤4)編號(hào)為Y(1≤Y≤7)的卡牌記為(X,Y).游戲可供3?5人玩,以下均以3人游戲?yàn)槔?在游戲的準(zhǔn)備階段,每位玩家會(huì)隨機(jī)的分到9張牌,剩余的一張牌牌面向下放置在桌上,稱為“殺手牌”.游戲的目標(biāo)是玩家猜出這張殺手牌是什么.游戲開始后由每個(gè)玩家輪流進(jìn)行行動(dòng),行動(dòng)可以是以下A0~A2中的一種:
(1)A0玩家說出一張牌,如果它是殺手牌,則游戲結(jié)束.
(2)A1玩家向其它玩家請(qǐng)求卡牌和放置卡牌,具體來講分為以下3步:
1)A1.1玩家向其他兩位玩家請(qǐng)求某個(gè)類型的牌.
2)A1.2其他兩位玩家如果手中有這種類型的牌,則選取一張牌面向下交給當(dāng)前玩家;如果手中沒有這種類型的牌,則告訴所有玩家.
3)A1.3當(dāng)前玩家根據(jù)手中的牌,如果出現(xiàn)3張不同花色但是相同序號(hào),或者3張相同花色并且連續(xù)序號(hào)的手牌時(shí),需要將其中兩張暗置,只暴露其中一張來進(jìn)行出牌;若手中沒有符合上述情形的三張手牌時(shí),只需出手牌中的任意一張,無需暗置.
(3)A2玩家查閱一張.
這個(gè)游戲的一個(gè)重要的問題是,在每個(gè)回合玩家都需要判斷目前的信息是否已經(jīng)能夠斷定哪一張牌是殺手牌.實(shí)際上,在經(jīng)過若干回合后,即使能夠記住每個(gè)回合的動(dò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個(gè)連續(xù)的編號(hào),同時(shí)也不存在某個(gè)編號(hào)的卡牌有3種類型.本文的工作就是使用邏輯工具來描述這個(gè)游戲的動(dòng)態(tài)過程,并且以此為基礎(chǔ)來進(jìn)行推理.
為了進(jìn)行游戲的推理,首先需要能夠描述這個(gè)動(dòng)態(tài)系統(tǒng).情景演算(situation calculus)是一種用來描述動(dòng)態(tài)系統(tǒng)的邏輯語言[4].它在一階邏輯的基礎(chǔ)上增加了狀態(tài)和動(dòng)作,因此可以用來描述在動(dòng)作的作用下不斷變化的系統(tǒng).情景演算中主要有3類元素:情景(situation),動(dòng)作(action)和實(shí)體流(fluent).實(shí)體流用來表示不同狀態(tài)下不同值的實(shí)體.
為了描述動(dòng)態(tài)系統(tǒng),在情景演算中包含以下的幾類約束:
(1)初始狀態(tài)和約束,例如在游戲的開始,需要描述每張牌可能在某個(gè)玩家手里或者是殺手牌,以及每個(gè)玩家恰好持有9張牌.
(2)描述動(dòng)作的前提和效果,例如某位玩家把一張牌放置在桌上的前提是這張牌這個(gè)回合在他手上,這個(gè)動(dòng)作的效果是在下個(gè)回合牌的位置在桌上.
(3)描述持續(xù)性的約束,例如一張牌如果在前一個(gè)回合在某個(gè)玩家手上,那么如果沒有相關(guān)的動(dòng)作,下個(gè)回合這張牌仍然應(yīng)該在這個(gè)玩家的手上.
游戲中,可以將每個(gè)玩家行動(dòng)開始的時(shí)候狀態(tài)作為一個(gè)情景,描述這個(gè)情景下的卡牌的位置需要滿足的約束,以及玩家實(shí)際的動(dòng)作所產(chǎn)生的約束等.為了更有效的實(shí)現(xiàn)系統(tǒng),我們直接使用命題邏輯的公式來描述了各種約束,以便隨后調(diào)用SMT[3]的求解器來求解.
可滿足模理論(Satisfiability Modulo Theory,SMT)是判斷一階邏輯公式在組合背景理論下的可滿足性問題[3].SMT的背景理論使其能很好地描述實(shí)際領(lǐng)域中的各種問題,結(jié)合高效的可滿足性判定算法,SMT在測(cè)試用例自動(dòng)生成、程序缺陷檢測(cè)驗(yàn)證[5]、RTL (Register Transfer Level)驗(yàn)證[6]、優(yōu)化問題求解[7,8]、靜態(tài)分析[9,10]、程序驗(yàn)證[11,12]等一些最新研究領(lǐng)域中有著突出的優(yōu)勢(shì).SMT求解技術(shù)的具體實(shí)現(xiàn)被稱為SMT求解器(SMT solvers).人們研發(fā)了很多SMT求解器,比較成熟的有Z3[13],CVC4[14],Yices2[15],MathSAT4[16],Boolector[17].其中,Z3是目前為止在擴(kuò)展性、表達(dá)能力以及求解效率等方面都較為出色的SMT求解器.它不僅可以用來驗(yàn)證多個(gè)邏輯公式的可滿足性,而且可以求出一組滿足約束的解.在本文中,我們使用2.2節(jié)所述方法編寫命題邏輯公式,調(diào)用Z3求解器來判斷公式的可滿足性.
假設(shè)玩家的數(shù)量為play_num,卡牌的類型為card_type,每類卡牌的數(shù)量為card_num,編號(hào)從1到card_num.類型為X編號(hào)為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編號(hào)為Y的卡牌.
4)0≤S≤play_num,S=0表示卡牌(X,Y)在桌上,否則表示卡牌在玩家S手中.
兩個(gè)描述動(dòng)作的謂詞:
(3)move(T,X,Y,P):在回合T卡牌移動(dòng)到了玩家P手中.
(4)put(T,X,Y):在回合T卡牌(X,Y)放到了桌上.
使用上述的描述狀態(tài)和動(dòng)作的謂詞,我們可以精確的描述游戲的每個(gè)回合的動(dòng)作和由此產(chǎn)生的狀態(tài)變化.由于本游戲是一個(gè)不完全信息游戲,因此在每個(gè)回合中,從不同的玩家視角看到的信息是不同.例如從玩家1的視角看,如果玩家2請(qǐng)求一張類型3的卡牌,那么玩家3交給玩家2的卡牌編號(hào)是未知的.
以下分別給出用來描述游戲中的動(dòng)作的邏輯公式.由于玩家視角的不同,相同的動(dòng)作由于獲得的信息不同,對(duì)應(yīng)的邏輯公式可能是不同的.
游戲開始記回合數(shù)t=0,如果玩家p分發(fā)到的卡牌為(x1,y1),…,(xn,yn)則增加公式:
確保所有的牌都發(fā)給了玩家,并且每個(gè)人都拿到了n張卡牌:
在每個(gè)回合的第一個(gè)階段是由當(dāng)前玩家向其他玩家請(qǐng)求一張線索牌.這里有3種情況:
(1)在回合t,玩家p1從玩家p2得到卡牌(x,y):
(2)在回合t,玩家p1從玩家p2得到類型x的卡牌,編號(hào)未知:
(3)在回合t,玩家p1從玩家p2請(qǐng)求類型x的卡牌,但是p2手中沒有類型x的卡牌:
在每個(gè)回合的第二階段是由當(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}是一個(gè)原子公式的集合,k∈N是一個(gè)自然數(shù),我們用AtMost(k,A)表示A中至多有k個(gè)公式為真,即如下的公式:
對(duì)于每個(gè)回合t,我們需要增加如下的公式來描述背景知識(shí).
(1)回合t有1個(gè)當(dāng)前玩家
(2)在回合t至多有n張牌移動(dòng)到來其它玩家手中
(3)在回合t至多有n張牌放置在桌上
(4)回合t結(jié)束時(shí)卡牌的位置
推理殺手牌的過程如算法1所示.定義一個(gè)SMT求解器Z3,將每回合產(chǎn)生的約束對(duì)應(yīng)的邏輯公式添加到Z3.在回合0,根據(jù)初始卡牌將式(1)和式(2)加入Z3.從回合1開始讀入數(shù)據(jù),并判斷在每個(gè)回合是否能夠確定殺手牌.如果Z3求解器返回SAT,說明有符合約束的解,如果將某一可能的殺手牌約束為非殺手牌后返回了UNSAT,說明該殺手牌是唯一可能的殺手牌,則返回該殺手牌,否則進(jìn)行下一回合.
算法1.推理殺手牌的過程?1 Φ= ;2 t=0;// 回合0 3 根據(jù)初始卡牌將公式(1)和式(2)加入Φ;4 t=1;// 從回合1開始讀入數(shù)據(jù),并判斷再每個(gè)回5合是否能夠確定殺手牌6 while讀取回合t的信息do 7 根據(jù)回合t的動(dòng)作,將公式(3)–(9)加入Φ;8 將回合t的背景知識(shí)公式(10)–(13)加入Φ;9 if check(Φ)=UNSAT then 10 返回錯(cuò)誤;// 讀入數(shù)據(jù)有誤11 else 12 M是Φ的一個(gè)模型;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;// 進(jìn)行下一回合
本文除了解決“誰是殺手”游戲推理問題外,還對(duì)游戲進(jìn)行了簡(jiǎn)單實(shí)現(xiàn).玩家可以登錄網(wǎng)頁(yè)進(jìn)行人機(jī)對(duì)戰(zhàn).系統(tǒng)包括客戶端和服務(wù)端兩部分,系統(tǒng)框架如圖1所示.游戲玩家在客戶端登陸,與服務(wù)端的AI玩家進(jìn)行PK.
圖1 系統(tǒng)框架圖
游戲玩家登陸網(wǎng)頁(yè)后,點(diǎn)擊“準(zhǔn)備”按鈕,客戶端進(jìn)行初始化,并向服務(wù)端發(fā)送請(qǐng)求,服務(wù)端接收到后,模擬發(fā)牌操作,將手牌發(fā)給客戶端.當(dāng)客戶端接收后,解析并將收到的手牌信息顯示給玩家.接著玩家可以根據(jù)游戲狀態(tài)點(diǎn)擊“問牌”、“看牌”、“出牌”、“給牌”、“猜牌”按鈕進(jìn)行相應(yīng)操作.服務(wù)端接收到客戶端動(dòng)作消息后模擬AI用戶做出應(yīng)答操作.
在服務(wù)端中,不僅要響應(yīng)客戶端的請(qǐng)求,還要模擬AI玩家游戲過程,進(jìn)行“猜牌”、“問牌”、“給牌”、“出牌”、“看牌”這些操作.當(dāng)輪到AI玩家給牌時(shí),判斷是否持有符合要求的卡牌,有則打出卡牌;當(dāng)輪到AI玩家看牌時(shí),隨機(jī)選擇某個(gè)回合放置在桌面的未知卡牌進(jìn)行查看;當(dāng)輪到AI玩家出牌時(shí),隨機(jī)打出符合要求的卡牌;當(dāng)輪到AI玩家問牌時(shí),隨機(jī)選擇一張未知卡牌.服務(wù)端會(huì)以AI玩家的視角,記錄游戲過程.AI玩家的推理過程如算法1所示.
本文提出了一種基于SMT的不完全信息游戲求解方法并基于此方法實(shí)現(xiàn)了一個(gè)“誰是殺手”游戲應(yīng)用,該應(yīng)用提供了一個(gè)能進(jìn)行人機(jī)交互對(duì)戰(zhàn)的網(wǎng)頁(yè)平臺(tái).游戲用戶在客戶端登陸便可與服務(wù)器端的AI進(jìn)行游戲?qū)?zhàn).AI玩家能夠應(yīng)用Z3求解器推理出殺手牌,但在問牌和出牌游戲動(dòng)作時(shí),沒有添加任何優(yōu)化策略,只是能夠打出符合規(guī)則的手牌,不會(huì)去考慮游戲的利益關(guān)系,處于一種“初級(jí)”玩家的智能水平.因此,下一步研究?jī)?nèi)容是通過優(yōu)化AI玩家問牌和出牌策略,使“出牌”的次數(shù)盡量少,同時(shí)獲得的線索信息盡可能更多,從而加強(qiáng)AI玩家的智能程度,加快推理過程.
計(jì)算機(jī)系統(tǒng)應(yīng)用2020年1期