《參數複雜性、SAT求解器和樹寬度》是依託上海交通大學，由陳翌佳擔任項目負責人的面上項目。
基本介紹
- 中文名：參數複雜性、SAT求解器和樹寬度
- 項目類別：面上項目
- 項目負責人：陳翌佳
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
參數複雜性是目前在理論計算機科學中非常活躍的一個分支。相比以多項式時間算法為核心的經典算法和複雜性理論，通過允許超多項式行為局限於某些小參數的指數時間算法，它為算法設計提供了更多的靈活性和複雜性分析更為精細的框架。我們計畫研究以下的一些基於樹寬度的比較新穎的參數複雜性問題。(1)SAT問題在工業界有著極為重要的套用。雖然其在一般意義上是NP難的，但許多SAT問題的求解器在實際使用中非常高效。我們計畫從參數複雜性角度來分析這些SAT求解器。特別的是，我們希望理解對於實際套用中出現的SAT實例是否存在一些隱藏的參數，它們導致求解器的高效。該研究一個很好的起點就是樹寬度有界的實例。(2)對於很多參數計算問題，樹寬度給出了高效可解和計算困難間的精確邊界。但還有一些關於樹寬度及其相關的算法問題仍有待解決。如：我們希望研究刪點操作對樹寬度的影響；針對程式語言的研究，我們試圖給出樹寬度有界圖的公理系統；為了理解monadic二階邏輯(MSO)的表達能力，我們計畫考察獨立於序的MSO。
結題摘要
本項目的主題是參數複雜性、SAT求解器和樹寬度的研究，其總體目標是利用參數複雜性的觀點來分析一些基於邏輯和圖論問題比經典複雜性更精細的算法和複雜性。在參數複雜性框架下每個計算問題的輸入都包含了一部分較小的參數，例如邏輯問題中的邏輯公式和圖論問題中所求節點集的大小。作為主要結果，我們在以下幾個問題上取得重要進展。 1. 我們解決了基於樹寬度的子圖同構問題參數複雜性猜想的重要特例-grid圖和wall圖。子圖同構問題包含了很多自然的算法圖論問題，如團問題、路徑問題。因此理解它的複雜性有重要的理論和套用價值。人們猜想這個問題難易完全取決於子圖的樹寬度。我們的結果對徹底理解這個問題又邁出了重要的一步。 2. 對於SAT問題我們證明了如果不可滿足的CNF公式的incidence graph的樹寬度有界，那么它就等價於一個有FPT大小消解證明的3CNF公式，這為理解SAT求解器在樹寬度有界的CNF公式上的行為建立了一定的基礎。 3. 我們證明了參數支配集問題的常數近似是W[1]難的。支配集問題是一個重要的NP完全的圖論問題，它的參數版本是W[2]完全的。目前關於它的一個重要研究方向是參數近似算法，即在固定參數時間下能否就算一個接近最優解的支配集。我們的結果是這個領域的一個重要進展。 4. 我們研究了一些比FPT更小的參數複雜性類，包括參數對數空間和參數AC0類，建立一系列圖論和邏輯問題相對這些類的上下界。相比固定參數可解類(FPT)，關於這些類的研究還處於初級階段。我們得到相對於參數AC0類幾個下界是這個方向最早的一批結果。而對於參數對數空間，我們建立著名的Savitch定理和參數空間複雜性的關聯。
