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

李炳坤 陳 寅

(華南師范大學計算機科學與技術系 廣東 廣州 510000)

0 引 言

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

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

1 問題描述

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

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

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

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

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

表1 Agent對物品偏好程度表

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

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

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

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

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

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

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

定義4(嫉妒程度最小化，MIN-ENY) 對于資源分配問題(P,G,Σ,E)，找到一個分配A使得嫉妒程度最小。一個分配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社交網絡如圖1所示。

圖1 Agent的社交網絡

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

考慮分配A2:

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

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

可以發現，A2不是一個局部無嫉妒分配，因為對于{p4,p5}∈E2，可以發現：

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

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

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

考慮分配A3:

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

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

因為對于{p3,p4}∈E2，可以發現:

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

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

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

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

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

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

則Agent社交網絡如圖2所示。

圖2 Agent的社交網絡

即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

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

在這4類問題中，EXT-LEF和EXT-REL是判定問題，MAX-AGT和MIN-ENY是優化問題。EXT-LEF研究給定的資源分配問題是否存在局部無嫉妒分配。MAX-AGT和MIN-ENY根據不同的目標函數來找到一個最接近局部無嫉妒分配的分配方案。EXT-REL是研究是否存在一個Agent在社交網絡上的重新分布方案，使得重新分布Agent后，新的社交網絡存在局部無嫉妒分配。

根據文獻[4]的結果，EXT-LEF和EXT-REL是NP完全問題，即使這個社交網絡是對于一些特定的圖，例如線性網絡、環或者是匹配圖。下文將資源分配問題的求解轉化為一個SMT問題。

2 基于SMT的問題求解

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

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

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

圖3 Z3求解框架

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

(declare-fun weight(Int Int) Int)

對于最終的分配，定義一個一元函數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約束用來確保每個Agent分配到不同的物品。上面定義的變量和函數沒有關于Agent的社交網絡的信息，事實上，有關的信息是在下面添加約束的時候體現出來的。

無嫉妒分配的存在性(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表達式。一個ite表達式形如:

(ite cond value1 value2)

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

對每一個Agentpi，假設所有包含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是一個局部無嫉妒的Agent，則cond_pi為真，否則為假。無嫉妒Agent最大化可以表達為如下的約束:

(maximize (sum

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

))

嫉妒程度最小化(MIN-ENY):對于每一條邊{pi,pj}∈E，它所產生的嫉妒程度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))))

)

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

(minimize

(sum env_1,…,env_k)

)

重排的可能性(EXT-REL):為了描述重排的雙射函數L:P→P，定義如下的一元函數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)

)

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

(declare-fun rf (Int) Int)

(declare-fun u () Int)

(declare-fun v () Int)

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

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

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

(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 實 驗

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

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

表2 測試用例平均運行時間 s

表2給出的是局部無嫉妒分配的存在性問題(EXT-LEF)的實驗數據。具有運行時間的測試用例，表示存在局部無嫉妒分配?？梢钥闯?，隨著Agent和物品數量的增加以及網絡稠密程度的提高，運行時間有了顯著的提高。另外，從原始的實驗數據可以發現，對于相同的Agent數量和相同的網絡稠密程度，在不同的隨機測試用例上的運行時間也是可能存在很大的差別。

本文針對稀疏的網絡也做了一些測試。圖4是對于不同的Agent和物品的數量在邊數比例分別為5%和10%下的運行時間的數據?？梢钥闯觯词故窍∈璧木W絡，隨著Agent和物品數量的增加，運行時間增加也很快，這是由問題本身的復雜性決定的。

圖4 稀疏網絡稠密程度影響

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

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

4 結 語

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

在今后的工作中，一方面可以考慮是否能夠直接實現一個高效的不可分物品的局部無嫉妒資源分配問題的求解系統，與基于SMT的系統相比有何優劣;另一方面，也可以從這個問題出發，考慮SMT求解器是否有可能進行適當的優化，以提高求解這類問題，特別是優化問題的效率。