《布爾可滿足性算法和單調布爾函式的複雜性》是依託上海交通大學，由Dominik Scheder擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：布爾可滿足性算法和單調布爾函式的複雜性
- 項目類別：青年科學基金項目
- 項目負責人：Dominik Scheder
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
本項目的第一個目標是改善當前布爾公式可滿足性（SAT）的算法。SAT是NP完全問題並且極有可能不存在解決SAT問題的亞指數時間算法。值得注意的是，我們完全不清楚PPSZ在最壞情況下的運行時間。PPSZ是目前最快的K-SAT算法。該項目試圖掃除這一盲障。這將需要更好更緊的上下界（如困難實例）和更嚴謹且可能更複雜的算法分析，並可能能夠顯著提高運行時間。..第二個目標是研究單調布爾函式的複雜性。其中，一個研究重點是函式的平均靈敏度和最大靈敏度。另一個重點是單調函式的單調電路複雜性。例如，無界單調電路的指數下界（Razborov, 1985）和在恆定深度電路上的超多項式下界（Ajtai, Gurevich, 1987）。在這個項目中，我們將在一些新方向上進行研究：由單調電路導致的函式的不可近似性; 將超多項式下界提升為指數下界; 考慮其他類別的電路，如對數深度（單調NC1）的單調電路.
結題摘要
該項目專注於研究 NP 完全可滿足性問題（SAT）的算法。 SAT 是邏輯上的決策問題，在理論和實踐中都很重要。 然而，現在幾乎沒有能夠快速解決 SAT 的方法; 因此，研究界有兩種思路：(a) 並非尋找一種在任何情況下都表現良好的方法，而是找到具有實踐意義的方法（啟發式）；(b) 找到能顯著改善平凡窮舉搜尋的方法，並研究哪些類別的 SAT 問題可以運用這些方法（中等指數算法）。 該項目側重於 (b)。 屬於理論研究（專注於數學證明，沒有實驗評估）。 我們在簡化和改善現有技術水平上做出了重要貢獻。
