近日,上海交通大學電子資訊與電氣工程學院電腦系長聘教軌副教授Dominik Scheder在理論電腦領域中最重要的NP完全問題k-SAT問題上的研究取得了重大進展——得到了目前為止最好的NP完全問題求解時間複雜度界。相關成果“PPSZ is better than you think”已被理論電腦界的頂級會議IEEE Symposium on Foundations of Computer Science(FOCS)2021接收。Dominik Scheder為論文的唯一作者。
該論文首次指出了1998年對PPSZ算灋的分析是次優的,且在未對算灋本身做任何修改的前提下給出了一個更加完全的算灋複雜度分析。該論文為後續研究PPSZ算灋真實時間複雜度分析奠定了基礎。
本研究由國家自然科學基金下的項目“布林可滿足性算灋和單調布林函數的複雜性”提供支援。
研究背景
布林可滿足性問題(SAT)是NP問題中的重要成員,是一類重要的確定性優化問題。
圖1 3-CNF公式(SAT問題舉例)
論文題目“PPSZ is better than you think”中提到的PPSZ算灋是用於求解SAT問題的經典算灋,由Paturi,Pudlak,Saks和Zane在1998年提出。PPSZ算灋的覈心思想是通過對解的編碼的求解來對實現SAT問題的求解。具體的執行過程如下:首先,給定一組布林變數,並對進行隨機重排列,記為。其中,對於可以根據特殊規則確定的,無需考慮它們的取值選取。隨機選取t個比特對剩餘的t個進行隨機賦值,將賦值後的作為概率性SAT算灋的輸入,輸出的t個隨機比特恰好對應解的概率為,這裡的t個隨機比特也稱為解的編碼比特。
作者Paturi,Pudlak,Saks和Zane給出的對PPSZ算灋的原始的複雜度分析方法是,通過判斷解的編碼比特的長度,得到PPSZ算灋的複雜度。而Hansen,Kaplan,Zamir和Zwick在STOC 2019上發表的論文中提到,可以通過將PPSZ算灋的輸入修改有傾向性隨機比特,提高PPSZ算灋的求解效率。
創新成果
本論文改進了PPSZ算灋的複雜度分析方法,得到了一個更優的時間複雜度界。作者優化該複雜度分析方法的主要優化思路是:按一種特定的分佈對布林變數進行賦值,而非直接均勻隨機地對其賦值。此時,我們可以得到一個更短的編碼;不需要真實對進行採樣賦值,只需類比描繪的賦值隨機性即可。
具體的分析過程類似於對樹的路徑滅絕問題的分析:
圖2:二叉樹的路徑滅絕:左邊的樹有可以避開所有紅色節點走到葉子節點的路徑;右邊的樹不存在這種路徑,稱之為二叉樹的路徑滅絕
FOCS由IEEE電腦學會的電腦數學基礎專委會提供資助,是計算機科學領域最頂級的國際會議,並被公認屬於難度最高的會議之一,與ACM計算理論年會(STOC)並稱理論計算機科學兩大頂會。FOCS會議涵蓋的領域十分廣泛,包括算灋和資料結構、計算複雜性、密碼學、計算幾何、算灋圖論與組合學、計算隨機性、計算博弈論和量子計算等。
FOCS的前身為1960年成立的開關電路理論與邏輯設計研討會(Symposium on Switching Circuit Theory and Logical Design),在1966年舉行的第7次會議時,名稱改為開關和自動機理論研討會(Symposium on Switching and Automata Theory,SWAT),1975年更名為IEEE計算機科學基礎研討會(IEEE Symposium on Foundations of Computer Science,FOCS)。
作者介紹
Dominik Scheder,電子資訊與電氣工程學院計算機科學與工程系長聘教軌副教授,2011年獲瑞士蘇黎世理工學院博士學位。曾先後在丹麥奧爾胡斯大學,加州大學伯克利分校西蒙研究所,清華大學任博士後研究學者。2014年加入上海交大電腦系工作。