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

李 健,郑荣基,汤宇锋,袁立然,陈 寅

(华南师范大学 计算机学院,广州 510631)

1 概述

计算机博弈(也称机器博弈)是人工智能领域的重要研究方向,是测试人工智能所达到水平的一个重要平台.它以人工智能和各种计算机博弈技术为基础,研究如何让计算机像人类一样从事高度智能的博弈活动.根据掌握的信息完全程度不同,计算机博弈可分为完全信息博弈和非完全信息博弈[1].在完全信息博弈领域,已有较为成熟的人工智能技术,最为出名的就是国际象棋领域的“深蓝”以及围棋领域的AlphaGo.而对于非完全信息博弈,由于博弈参与者掌握的信息有限,仅凭当前有限的信息无法准确推测对手所处的状态,更加难以准确推断与估计对手的决策行为,在研究上有相当大的复杂性和不确定性.2017年1月,才由卡内基梅隆大学研发的Libratus人工智能系统在德州扑克中战胜人类玩家,之后鲜有其他人工智能系统攻克非完全信息博弈.

目前,整个非完全信息博弈的研究还处于初级阶段.但是,在现实生活中大到国家,小到家庭,人们面临的诸多问题都是以非完全信息的形式存在着.因此,非完全信息博弈的研究目的和意义所在,便是如何在已知的有限的信息的前提下,为人类的生活和发展提供指导,以谋求最大的利益.现在,科技高速发展,移动互联网发展更为迅猛,让人工智能和计算机博弈的发展更加的多元化.人们的碎片化时间越来越多,阅读、玩游戏等等成了人们娱乐消遣的主要方式.很多时候,玩家都是在和计算机博弈程序进行博弈[2].针对这一种现象,很多游戏产商将游戏中的人工智能放在业务重心之一.

“谁是杀手”是一种非完全信息的推理游戏,其要求玩家根据自己手中的牌以及游戏过程中所获得的相关信息推理出杀手牌.本文以“谁是杀手”游戏为例,研究了一种基于SMT[3]的不完全信息游戏求解方法,旨在对非完备信息博弈进行学习与研究,同时设计并实现了一个能进行人机交互对战的网页平台.

2 背景知识

2.1 游戏简介

“谁是杀手”游戏(以下简称为“游戏”)是一种规则简单同时又需要推理的卡牌游戏.游戏共有28张卡牌,分为四类,每类卡牌的编号为1至7.以下我们把类型为X(1≤X≤4)编号为Y(1≤Y≤7)的卡牌记为(X,Y).游戏可供3−5人玩,以下均以3人游戏为例.在游戏的准备阶段,每位玩家会随机的分到9张牌,剩余的一张牌牌面向下放置在桌上,称为“杀手牌”.游戏的目标是玩家猜出这张杀手牌是什么.游戏开始后由每个玩家轮流进行行动,行动可以是以下A0～A2中的一种:

(1)A0玩家说出一张牌,如果它是杀手牌,则游戏结束.

(2)A1玩家向其它玩家请求卡牌和放置卡牌,具体来讲分为以下3步:

1)A1.1玩家向其他两位玩家请求某个类型的牌.

2)A1.2其他两位玩家如果手中有这种类型的牌,则选取一张牌面向下交给当前玩家;如果手中没有这种类型的牌,则告诉所有玩家.

3)A1.3当前玩家根据手中的牌,如果出现3张不同花色但是相同序号,或者3张相同花色并且连续序号的手牌时,需要将其中两张暗置,只暴露其中一张来进行出牌;若手中没有符合上述情形的三张手牌时,只需出手牌中的任意一张,无需暗置.

(3)A2玩家查阅一张.

这个游戏的一个重要的问题是,在每个回合玩家都需要判断目前的信息是否已经能够断定哪一张牌是杀手牌.实际上,在经过若干回合后,即使能够记住每个回合的动作,由人脑来推断是否可以断定杀手牌也是很困难的.例如,在A1.3中如果玩家放置了3张牌,其中暴露的牌是(2,3),按照规则玩家放置的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中,如果玩家只放置了一张牌,能够用于推理的信息则更加复杂.它表示玩家手中没有任何类型的卡牌有3个连续的编号,同时也不存在某个编号的卡牌有3种类型.本文的工作就是使用逻辑工具来描述这个游戏的动态过程,并且以此为基础来进行推理.

2.2 动态系统的逻辑描述

为了进行游戏的推理,首先需要能够描述这个动态系统.情景演算(situation calculus)是一种用来描述动态系统的逻辑语言[4].它在一阶逻辑的基础上增加了状态和动作,因此可以用来描述在动作的作用下不断变化的系统.情景演算中主要有3类元素:情景(situation),动作(action)和实体流(fluent).实体流用来表示不同状态下不同值的实体.

为了描述动态系统,在情景演算中包含以下的几类约束:

(1)初始状态和约束,例如在游戏的开始,需要描述每张牌可能在某个玩家手里或者是杀手牌,以及每个玩家恰好持有9张牌.

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

(3)描述持续性的约束,例如一张牌如果在前一个回合在某个玩家手上,那么如果没有相关的动作,下个回合这张牌仍然应该在这个玩家的手上.

游戏中,可以将每个玩家行动开始的时候状态作为一个情景,描述这个情景下的卡牌的位置需要满足的约束,以及玩家实际的动作所产生的约束等.为了更有效的实现系统,我们直接使用命题逻辑的公式来描述了各种约束,以便随后调用SMT[3]的求解器来求解.

2.3 SMT及其求解器

可满足模理论(Satisfiability Modulo Theory,SMT)是判断一阶逻辑公式在组合背景理论下的可满足性问题[3].SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测验证[5]、RTL (Register Transfer Level)验证[6]、优化问题求解[7,8]、静态分析[9,10]、程序验证[11,12]等一些最新研究领域中有着突出的优势.SMT求解技术的具体实现被称为SMT求解器(SMT solvers).人们研发了很多SMT求解器,比较成熟的有Z3[13],CVC4[14],Yices2[15],MathSAT4[16],Boolector[17].其中,Z3是目前为止在扩展性、表达能力以及求解效率等方面都较为出色的SMT求解器.它不仅可以用来验证多个逻辑公式的可满足性,而且可以求出一组满足约束的解.在本文中,我们使用2.2节所述方法编写命题逻辑公式,调用Z3求解器来判断公式的可满足性.

3 推理的实现

假设玩家的数量为play_num,卡牌的类型为card_type,每类卡牌的数量为card_num,编号从1到card_num.类型为X编号为Y的卡牌记为(X,Y).

为了描述状态,需要以下的谓词:

(1)turn(T,P):回合T的当前玩家是玩家P.

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

1)T∈N,表示回合数.

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)放到了桌上.

使用上述的描述状态和动作的谓词,我们可以精确的描述游戏的每个回合的动作和由此产生的状态变化.由于本游戏是一个不完全信息游戏,因此在每个回合中,从不同的玩家视角看到的信息是不同.例如从玩家1的视角看,如果玩家2请求一张类型3的卡牌,那么玩家3交给玩家2的卡牌编号是未知的.

以下分别给出用来描述游戏中的动作的逻辑公式.由于玩家视角的不同,相同的动作由于获得的信息不同,对应的逻辑公式可能是不同的.

游戏开始记回合数t=0,如果玩家p分发到的卡牌为(x1,y1),…,(xn,yn)则增加公式:

确保所有的牌都发给了玩家,并且每个人都拿到了n张卡牌:

在每个回合的第一个阶段是由当前玩家向其他玩家请求一张线索牌.这里有3种情况:

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

(2)在回合t,玩家p1从玩家p2得到类型x的卡牌,编号未知:

(3)在回合t,玩家p1从玩家p2请求类型x的卡牌,但是p2手中没有类型x的卡牌:

在每个回合的第二阶段是由当前玩家放牌在桌上.这里有四种情况:

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

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

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

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

如果A={a1,…,an}是一个原子公式的集合,k∈N是一个自然数,我们用AtMost(k,A)表示A中至多有k个公式为真,即如下的公式:

对于每个回合t,我们需要增加如下的公式来描述背景知识.

(1)回合t有1个当前玩家

(2)在回合t至多有n张牌移动到来其它玩家手中

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

(4)回合t结束时卡牌的位置

推理杀手牌的过程如算法1所示.定义一个SMT求解器Z3,将每回合产生的约束对应的逻辑公式添加到Z3.在回合0,根据初始卡牌将式(1)和式(2)加入Z3.从回合1开始读入数据,并判断在每个回合是否能够确定杀手牌.如果Z3求解器返回SAT,说明有符合约束的解,如果将某一可能的杀手牌约束为非杀手牌后返回了UNSAT,说明该杀手牌是唯一可能的杀手牌,则返回该杀手牌,否则进行下一回合.

算法1.推理杀手牌的过程∅1 Φ= ;2 t=0;// 回合0 3 根据初始卡牌将公式(1)和式(2)加入Φ;4 t=1;// 从回合1开始读入数据,并判断再每个回5合是否能够确定杀手牌6 while读取回合t的信息do 7 根据回合t的动作,将公式(3)–(9)加入Φ;8 将回合t的背景知识公式(10)–(13)加入Φ;9 if check(Φ)=UNSAT then 10 返回错误;// 读入数据有误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 系统实现

本文除了解决“谁是杀手”游戏推理问题外,还对游戏进行了简单实现.玩家可以登录网页进行人机对战.系统包括客户端和服务端两部分,系统框架如图1所示.游戏玩家在客户端登陆,与服务端的AI玩家进行PK.

图1 系统框架图

4.1 客户端

游戏玩家登陆网页后,点击“准备”按钮,客户端进行初始化,并向服务端发送请求,服务端接收到后,模拟发牌操作,将手牌发给客户端.当客户端接收后,解析并将收到的手牌信息显示给玩家.接着玩家可以根据游戏状态点击“问牌”、“看牌”、“出牌”、“给牌”、“猜牌”按钮进行相应操作.服务端接收到客户端动作消息后模拟AI用户做出应答操作.

4.2 服务端

在服务端中,不仅要响应客户端的请求,还要模拟AI玩家游戏过程,进行“猜牌”、“问牌”、“给牌”、“出牌”、“看牌”这些操作.当轮到AI玩家给牌时,判断是否持有符合要求的卡牌,有则打出卡牌;当轮到AI玩家看牌时,随机选择某个回合放置在桌面的未知卡牌进行查看;当轮到AI玩家出牌时,随机打出符合要求的卡牌;当轮到AI玩家问牌时,随机选择一张未知卡牌.服务端会以AI玩家的视角,记录游戏过程.AI玩家的推理过程如算法1所示.

5 总结与展望

本文提出了一种基于SMT的不完全信息游戏求解方法并基于此方法实现了一个“谁是杀手”游戏应用,该应用提供了一个能进行人机交互对战的网页平台.游戏用户在客户端登陆便可与服务器端的AI进行游戏对战.AI玩家能够应用Z3求解器推理出杀手牌,但在问牌和出牌游戏动作时,没有添加任何优化策略,只是能够打出符合规则的手牌,不会去考虑游戏的利益关系,处于一种“初级”玩家的智能水平.因此,下一步研究内容是通过优化AI玩家问牌和出牌策略,使“出牌”的次数尽量少,同时获得的线索信息尽可能更多,从而加强AI玩家的智能程度,加快推理过程.