基于SMT的局部無嫉妒資源分配問題求解

李炳坤 陳 寅

(華南師范大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系 廣東 廣州 510000)

0 引 言

公平分配問題最初來源于經(jīng)濟(jì)學(xué)和政治學(xué)。目前在人工智能、計(jì)算機(jī)科學(xué)和應(yīng)用數(shù)學(xué)等多個(gè)研究領(lǐng)域都得到關(guān)注。根據(jù)需要分配物品的不同，公平分配問題可以分為可分物品(divisible goods)的分配和不可分物品(indivisible goods)的分配。例如，切蛋糕問題是一個(gè)經(jīng)典的可分物品的分配問題[7]，而房屋分配問題顯然是一個(gè)不可分物品的分配問題[1]。對于分配是否公平也存在多種解釋[9]，例如均衡性(proportional)是指對于n個(gè)Agent而言，每個(gè)Agent都認(rèn)為自己分到至少1/n的物品，而無嫉妒分配(envy-free)是指每個(gè)Agent都認(rèn)為自己獲得的物品都不少于其他人。最近的一些研究中開始討論Agent或者需要分配的物品之間可能存在的某種關(guān)聯(lián)。例如文獻(xiàn)[8]中討論了物品之間存在某種依賴關(guān)系的分配問題，而文獻(xiàn)[4]中討論了Agent之間存在社交網(wǎng)絡(luò)的分配問題。

在計(jì)算機(jī)科學(xué)和人工智能領(lǐng)域，公平分配問題的研究主要是相關(guān)問題的計(jì)算復(fù)雜度和算法實(shí)現(xiàn)。本文研究的問題是如何在一個(gè)社交網(wǎng)絡(luò)中進(jìn)行不可分貨物的無嫉妒分配，文中對研究的問題做一些限定。假設(shè)每個(gè)Agent都對物品有不同偏好，這個(gè)偏好通過對每個(gè)物品賦一個(gè)權(quán)重來體現(xiàn)。這里約定權(quán)重越小對應(yīng)于偏好的程度越高。每個(gè)Agent只能被分配一個(gè)物品，因此Agent的人數(shù)不能大于物品的人數(shù)。對于這類問題，如果分配是無嫉妒的，那么每個(gè)Agent都需要分配到對自己而言權(quán)重最小的物品。如果考慮到Agent處于一個(gè)社交網(wǎng)絡(luò)中，并且只關(guān)心和它相鄰的Agent分配的物品，那么在考慮無嫉妒分配的時(shí)候，情況就會有所不同。最近的研究[8]中給出這類問題的一些算法的結(jié)果。本文主要工作是給出上述分配問題求解的實(shí)現(xiàn)，并給出一些實(shí)驗(yàn)結(jié)果。

1 問題描述

假設(shè)有一個(gè)Agent的集合P={p1,p2,…,pn}和一個(gè)物品的集合G={g1,g2,…,gm}，其中n≤m。文中

規(guī)定n個(gè)Agent每人分一件物品，同時(shí)用Σ={σ1,σ2，…,σn}表示每個(gè)Agent對不同物品的偏好，其中σi(1≤i≤n)是G到N+的函數(shù)，σi(gi)的數(shù)值越小表示對于物品gi喜好程度越高。Agent之間的社交網(wǎng)路用無向圖來表示，E是無序?qū)pi,pj}的集合，pi,pj∈P。本文用四元組(P,G,Σ,E)來表示一個(gè)資源分配問題。

定義1對于資源分配問題(P,G,Σ,E)，分配是一個(gè)單射函數(shù)A:P→G，表示每一個(gè)Agent分配一個(gè)不同的物品。如果對任意兩個(gè)Agentpi和pj都滿足σi(A(pi))≤σi(A(pj)),則稱分配A是無嫉妒的(envy-free)。如果對兩個(gè)Agent{pi,pj}∈E，都滿足σi(A(pi))≤σi(A(pj))，則稱分配A是局部無嫉妒的(local envy-free)。

顯然，如果一個(gè)分配是無嫉妒的，那么它一定是局部無嫉妒的，但是在一般的情況下，無嫉妒分配是困難的。例如，考慮Agent的數(shù)量和物品數(shù)量相等，并且每個(gè)Agent對物品的評價(jià)都是嚴(yán)格有序的，那么除非每個(gè)Agent都被分配到最喜好的物品，否則無嫉妒分配是不存在的。如果考慮特定的社交網(wǎng)絡(luò)下的資源分配問題，那么找到一個(gè)局部無嫉妒分配要相對容易得多，因?yàn)槊總€(gè)Agent只需要得到比相鄰Agent更好的物品即可。

例1考慮一個(gè)為6個(gè)Agent,P={p1,p2,p3,p4,p5,p6}分配6個(gè)物品G={g1,g2,g3,g4,g5,g6}的例子。假設(shè)Agent對物品的偏好Σ={σ1,σ2,σ3,σ4,σ5,σ6}，如表1所示。

表1 Agent對物品偏好程度表

對于E1={{p1,p2},{p3,p4},{p5,p6}},可以驗(yàn)證分配A1:

A1(p1)=g6,A1(p2)=g3,A1(p3)=g5,

A1(p4)=g2,A1(p5)=g1,A1(p6)=g4

這是(P,G,Σ,E)的一個(gè)局部無嫉妒的分配。

給定一個(gè)社交網(wǎng)路，首先關(guān)心一個(gè)資源分配問題是否存在局部無嫉妒的分配。如果這樣的分配不存在，那么如何找到一個(gè)分配能夠使得無嫉妒的Agent最多或者Agent的嫉妒程度最小。一般而言，分為4類無嫉妒分配的問題[4]。

定義2(無嫉妒分配的存在性，EXT-LEF) 對于資源分配問題(P,G,Σ,E)，是否存在一個(gè)局部無嫉妒分配。

定義3(無嫉妒Agent最大化，MAX-AGT) 對于資源分配問題(P,G,Σ,E)，找到一個(gè)分配A使得局部無嫉妒Agent的人數(shù)最大。一個(gè)Agentpi在A下是局部無嫉妒的，如果對任意的pj，{pi,pj}∈E，都有σi(A(pi))≤σi(A(pj))。

定義4(嫉妒程度最小化，MIN-ENY) 對于資源分配問題(P,G,Σ,E)，找到一個(gè)分配A使得嫉妒程度最小。一個(gè)分配A的嫉妒程度定義為:

其中:對于{pi,pj}∈E，e(A,pi,pj)=max(0,σi(A(pi))-σi(A(pj)))。

例2在例1中，考慮E2={{p1,p2},{p1,p3},{p2,p3},{p3,p4},{p4,p5},{p4,p6}}。Agent社交網(wǎng)絡(luò)如圖1所示。

圖1 Agent的社交網(wǎng)絡(luò)

可以驗(yàn)證，對于EXT-LEF問題而言，(P,G,Σ,E2)是不存在局部無嫉妒分配的。

考慮分配A2:

A2(p1)=g2,A2(p2)=g3,A2(p3)=g1,

A2(p4)=g5,A2(p5)=g6,A2(p6)=g4

可以發(fā)現(xiàn)，A2不是一個(gè)局部無嫉妒分配，因?yàn)閷τ趝p4,p5}∈E2，可以發(fā)現(xiàn)：

σ4(A2(p4))=σ4(g5)=6

σ4(A2(p5))=σ4(g6)=2

由于σ4(A2(p4))>σ4(A2(p5))，因此p4不是一個(gè)局部無嫉妒的。除了p4之外，剩余的5個(gè)Agent都是局部無嫉妒的Agent。因此A2是(P,G,Σ,E2)的一個(gè)MAX-AGT分配。

考慮分配A3:

A3(p1)=g1,A3(p2)=g3,A3(p3)=g4,

A3(p4)=g6,A3(p5)=g2,A3(p6)=g5

因?yàn)閷τ趝p3,p4}∈E2，可以發(fā)現(xiàn):

e(A3,p3,p4)+e(A3,p4,p3)=max(0,σ3(g4)-σ3(g6))+max(0,σ4(g6)-σ4(g4))=1

同時(shí)，對其余的{pi,pj}∈E2，均有e(A3,pi,pj)+e(A3,pj,pi)=0。因此分配A3的嫉妒程度為1。A3是(P,G,Σ,E2)的一個(gè)MIN-ENY分配。

定義5(重排的可能性，EXT-REL) 對于資源分配問題(P,G,Σ,E)，是否存在一個(gè)分配A和一個(gè)雙射函數(shù)L:P→P，使得對任意的邊{L(pi),L(pj)}∈E，都有σi(A(pi))≤σi(A(pj))。

例3對于例2中的問題(P,G,Σ,E2)，考慮雙射函數(shù)L1:P→P如下:

L1(p1)=p5,L1(p2)=p4,L1(p3)=p6

L1(p4)=p1,L1(p5)=p3,L1(p6)=p2

則Agent社交網(wǎng)絡(luò)如圖2所示。

圖2 Agent的社交網(wǎng)絡(luò)

即E3={{p1,p2},{p2,p3},{p2,p5},{p4,p5},{p4,p6},{p5,p6}}。

考慮分配A4:

A4(p1)=g5,A4(p2)=g3,A4(p3)=g6,

A4(p4)=g4,A4(p5)=g2,A4(p6)=g1

可以驗(yàn)證，A4是(P,G,Σ,E3)的一個(gè)局部無嫉妒分配，因此(P,G,Σ,E2)存在一個(gè)EXT-REL分配。

在這4類問題中，EXT-LEF和EXT-REL是判定問題，MAX-AGT和MIN-ENY是優(yōu)化問題。EXT-LEF研究給定的資源分配問題是否存在局部無嫉妒分配。MAX-AGT和MIN-ENY根據(jù)不同的目標(biāo)函數(shù)來找到一個(gè)最接近局部無嫉妒分配的分配方案。EXT-REL是研究是否存在一個(gè)Agent在社交網(wǎng)絡(luò)上的重新分布方案，使得重新分布Agent后，新的社交網(wǎng)絡(luò)存在局部無嫉妒分配。

根據(jù)文獻(xiàn)[4]的結(jié)果，EXT-LEF和EXT-REL是NP完全問題，即使這個(gè)社交網(wǎng)絡(luò)是對于一些特定的圖，例如線性網(wǎng)絡(luò)、環(huán)或者是匹配圖。下文將資源分配問題的求解轉(zhuǎn)化為一個(gè)SMT問題。

2 基于SMT的問題求解

SMT可稱為“可滿足性模理論”、“多理論下的可滿足性問題”或者“特定(背景)理論下的可滿足性問題”(參見綜述性的文獻(xiàn)[10])，它可以被認(rèn)為是一種SAT(satisfiability)的擴(kuò)展。一個(gè)SMT公式是包含背景理論的邏輯公式，例如SMT公式x>1∧y<3可以認(rèn)為是一個(gè)邏輯公式φ∧ψ，其中φ的真值由數(shù)學(xué)不等式x>1確定，ψ的真值由數(shù)學(xué)不等式y(tǒng)<3確定。通常，SMT問題是指判斷一個(gè)給定的SMT公式集是否是可滿足的。

SMT已經(jīng)在人工智能和計(jì)算機(jī)科學(xué)的很多問題上有了廣泛的應(yīng)用，同時(shí)目前已經(jīng)開發(fā)了很多SMT求解器用來求解SMT問題，例如Z3[5]、Yices[6]和CVC3/CVC4[2]等。輸入一個(gè)SMT問題，SMT求解器可以返回這個(gè)問題是否是可滿足的，對于可滿足的問題還會返回一個(gè)模型。

圖3說明如何使用Z3求解局部無嫉妒分配問題的模型框架。一個(gè)局部無嫉妒分配問題可轉(zhuǎn)換為一些邏輯公式和約束的解釋恰好對應(yīng)原問題的一個(gè)解，進(jìn)一步轉(zhuǎn)換為SMT格式的輸入，由Z3求得模型，即問題的解。

圖3 Z3求解框架

下面說明如何把求解局部無嫉妒的資源分配問題轉(zhuǎn)換為一個(gè)SMT問題。首先需要定義變量和約束來描述問題?？紤]n個(gè)Agent和m個(gè)貨物，用二元函數(shù)weight來表保存Agent對貨物的偏好:

(declare-fun weight(Int Int) Int)

對于最終的分配，定義一個(gè)一元函數(shù)alloc和如下的約束:

(declare-fun alloc (Int) Int)

(assert (and (>(alloc 1) 0) (<=(alloc 1) m)))

……

(assert (and (>(alloc n) 0) (<=(alloc n) m)))

(assert (

distinct (alloc 1) (alloc 2)…(alloc m)))

其中：(alloc i)表示為Agentpi分配的物品，0<(alloci)≤m；distinct約束用來確保每個(gè)Agent分配到不同的物品。上面定義的變量和函數(shù)沒有關(guān)于Agent的社交網(wǎng)絡(luò)的信息，事實(shí)上，有關(guān)的信息是在下面添加約束的時(shí)候體現(xiàn)出來的。

無嫉妒分配的存在性(EXT-LEF):對每一條邊{pi,pj}增加如下約束:

(assert (<=(weight i (alloc i))

(weight i (alloc j))))

(assert (<=(weight j (alloc j))

(weight j (alloc i))))

分別表示σi(A(pi))≤σi(A(pj))和σj(A(pj))≤σj(A(pi))。

無嫉妒Agent最大化(MAX-AGT):這里需要用到SMT的ite表達(dá)式。一個(gè)ite表達(dá)式形如:

(ite cond value1 value2)

其中：cond是一個(gè)邏輯公式，value1和value2為兩個(gè)值。如果cond為真，則表達(dá)式的值為value1，否則表達(dá)式的值為value2。

對每一個(gè)Agentpi，假設(shè)所有包含pi的邊為{pi,pj1},{pi,pj2},…,{pi,pjk}，cond_pi表示如下的邏輯公式:

(and

(<=(weight i (alloc i))

(weight i (alloc j1)))

……

(<=(weight i (alloc i))

(weight i (alloc jk)))

)

如果pi是一個(gè)局部無嫉妒的Agent，則cond_pi為真，否則為假。無嫉妒Agent最大化可以表達(dá)為如下的約束:

(maximize (sum

(ite cond_p1 1 0)……(ite cond_pn 1 0)

))

嫉妒程度最小化(MIN-ENY):對于每一條邊{pi,pj}∈E，它所產(chǎn)生的嫉妒程度e(A,pi,pj)+e(A,pj,pi)可以表示為:

(+

(ite

(<=(weight i (alloc i))

(weight i (alloc j)))

0

(-(weight i (alloc i))

(weight i (alloc j))))

(ite

(<=(weight j (alloc j))

(weight j (alloc i)))

0

(-(weight j (alloc j))

(weight j (alloc i))))

)

假設(shè)E中有k條邊，它們所產(chǎn)生的嫉妒程度分別是env_1,env_2,…,env_k，則嫉妒程度最小化的約束可以表示為：

(minimize

(sum env_1,…,env_k)

)

重排的可能性(EXT-REL):為了描述重排的雙射函數(shù)L:P→P，定義如下的一元函數(shù)realloc和約束：

(declare-fun realloc (Int) Int)

(assert (and (> (realloc 1) 0)

(<=(realloc 1) n)))

……

(assert (and (> (realloc n) 0)

(<=(realloc n) n)))

(assert (

distinct

(realloc 1) (alloc 2)…(realloc n)

)

同時(shí)，為了從L(pi)也能得到pi，定義一個(gè)輔助的一元函數(shù)rf如下:

(declare-fun rf (Int) Int)

(declare-fun u () Int)

(declare-fun v () Int)

(assert (<=> (=(realloc u) v) (=(rf v) u)))

利用這里的約束，實(shí)際上rf恰好是realloc的反函數(shù)。

最后，對于每一條邊{pi,pj}∈E，增加兩個(gè)約束:

(assert (<=(weight (rf i) (alloc (rf i)))

(weight (rf i) (alloc (rf j)))))

(assert (<=(weight (rf j) (alloc (rf j)))

(weight (rf j) (alloc (rf i)))))

3 實(shí) 驗(yàn)

本文使用了Z3實(shí)現(xiàn)了基于SMT的不可分物品的局部無嫉妒資源分配問題求解。Z3是微軟公司開發(fā)的一個(gè)開源的SMT求解器，也是目前最好的求解器之一。Z3不僅支持標(biāo)準(zhǔn)的SMT-LIBv2語言[3]，同時(shí)還提供了一些擴(kuò)展的功能。

文中使用Z3提供的Python接口z3py實(shí)現(xiàn)了系統(tǒng)。系統(tǒng)的代碼用Python 3.6和z3 4.8版本實(shí)現(xiàn)。所有的實(shí)驗(yàn)數(shù)據(jù)都是使用Ubuntu Linux 18.04LTS，在一臺3.6 GHz的Intel i7-7700和8 GB內(nèi)存的個(gè)人計(jì)算機(jī)上測得的。隨機(jī)生成一些不同規(guī)模的測試用例。在實(shí)驗(yàn)中，總是設(shè)定Agent的人數(shù)agent_num等于物品的個(gè)數(shù)goods_num。對于相同的Agent人數(shù)和物品個(gè)數(shù)，社交網(wǎng)絡(luò)的稠密程度對運(yùn)行時(shí)間也有顯著的影響。用網(wǎng)絡(luò)中邊數(shù)與相對應(yīng)的完全圖的邊數(shù)比例edge_ratio來衡量網(wǎng)絡(luò)的稠密程度，例如對于n個(gè)結(jié)點(diǎn)的社交網(wǎng)絡(luò)，邊數(shù)比例為5%的網(wǎng)絡(luò)是相對稀疏的，它的邊數(shù)為n(n-1)/2×5%。每個(gè)測試用例的超時(shí)時(shí)間設(shè)定為1 200秒。表2中，每一個(gè)運(yùn)行時(shí)間都是5個(gè)隨機(jī)測試用例運(yùn)行時(shí)間的均值，單位為秒。如果這5個(gè)測試用例中有一個(gè)超時(shí)，則這個(gè)運(yùn)行時(shí)間就設(shè)定為超時(shí)(表中為“-”)。

表2 測試用例平均運(yùn)行時(shí)間 s

表2給出的是局部無嫉妒分配的存在性問題(EXT-LEF)的實(shí)驗(yàn)數(shù)據(jù)。具有運(yùn)行時(shí)間的測試用例，表示存在局部無嫉妒分配。可以看出，隨著Agent和物品數(shù)量的增加以及網(wǎng)絡(luò)稠密程度的提高，運(yùn)行時(shí)間有了顯著的提高。另外，從原始的實(shí)驗(yàn)數(shù)據(jù)可以發(fā)現(xiàn)，對于相同的Agent數(shù)量和相同的網(wǎng)絡(luò)稠密程度，在不同的隨機(jī)測試用例上的運(yùn)行時(shí)間也是可能存在很大的差別。

本文針對稀疏的網(wǎng)絡(luò)也做了一些測試。圖4是對于不同的Agent和物品的數(shù)量在邊數(shù)比例分別為5%和10%下的運(yùn)行時(shí)間的數(shù)據(jù)?？梢钥闯?，即使是稀疏的網(wǎng)絡(luò)，隨著Agent和物品數(shù)量的增加，運(yùn)行時(shí)間增加也很快，這是由問題本身的復(fù)雜性決定的。

圖4 稀疏網(wǎng)絡(luò)稠密程度影響

對于MAX-AGT、MIN-ENY和EXT-REL等優(yōu)化問題，需要在有局部無嫉妒分配的測試樣例上進(jìn)行實(shí)驗(yàn)。根據(jù)表2中的結(jié)果，隨機(jī)產(chǎn)生一些Agent和物品數(shù)量在10到35之間，網(wǎng)絡(luò)稠密程度在30%到40%之間的測試用例。這些測試用例經(jīng)過EXT-LEF檢測，都不存在局部無嫉妒分配。表3中給出了這些測試用例計(jì)算MAX-AGT、MIN-ENY和EXT-REL的運(yùn)行時(shí)間。每一行的m-n-k表示Agent的數(shù)量，物品的數(shù)量和邊數(shù)比例，隨后的4個(gè)數(shù)字是相應(yīng)的資源分配問題的運(yùn)行時(shí)間。運(yùn)行時(shí)間仍然是5個(gè)隨機(jī)測試用例的均值。總體而言，與EXT-LEF相比，MAX-AGT、MIN-ENY和EXT-REL需要更長的運(yùn)行時(shí)間。

表3 局部無嫉妒分配的測試樣例 s

4 結(jié) 語

本文研究了不可分物品的局部無嫉妒資源分配問題。通過把這個(gè)問題轉(zhuǎn)化為SMT問題，實(shí)現(xiàn)一個(gè)基于Z3的系統(tǒng)。有關(guān)資源分配問題的相關(guān)研究主要集中于理論上的分析和有關(guān)復(fù)雜度的證明，具體的系統(tǒng)實(shí)現(xiàn)并不多見。初步嘗試證明了利用SMT求解器來求解這類NP難題的可能性，同時(shí)也發(fā)現(xiàn)隨著問題規(guī)模增長，求解的時(shí)間增長很快，特別是對于MAX-AGT和MIN-ENY這樣的優(yōu)化問題。

在今后的工作中，一方面可以考慮是否能夠直接實(shí)現(xiàn)一個(gè)高效的不可分物品的局部無嫉妒資源分配問題的求解系統(tǒng)，與基于SMT的系統(tǒng)相比有何優(yōu)劣;另一方面，也可以從這個(gè)問題出發(fā)，考慮SMT求解器是否有可能進(jìn)行適當(dāng)?shù)膬?yōu)化，以提高求解這類問題，特別是優(yōu)化問題的效率。