精簡表示的NP完全問題與相依量詞布林公式

Abstract

精簡表示是指以對數大小的方式表示原本的問題，通常會導致問題的複雜度指數級增長。目前對精簡表示問題的已知解法是將它們先展開成標準表示，但這個過程可能會失去精簡表示隱含的附加信息。

對於解決精簡表示的非確定性多項式時間完備（NP-complete）問題，我們特別感興趣於兩種可滿足性問題是非確定性指數時間完備（NEXP-complete）的邏輯框架：雙變量邏輯（FO2）和相依量詞布林公式（DQBF）。雙變量邏輯為一階邏輯使用至多兩個變數的可判定（decidable）子集。相依量詞布林公式是廣義化的布林公式，可應用在軟硬體設計的驗證和合成中，近年來在求解方面已經取得了顯著進展。我們想要了解雙變量邏輯和相依量詞布林公式的求解器是否可用於幫助解決精簡表示的非確定性多項式時間完備問題。

本論文提出了從精簡表示的非確定性多項式時間完備問題到雙變量邏輯和相依量詞布林公式的規約（reduction）。我們還提出了用於求解相依量詞布林公式的演算法，該演算法在一些不可滿足的實例上比起已知的標準方法更具優勢。為了展示不同解法的效力，本文介紹了兩個具有精簡表示的圖列，並展示了它們在獨立集問題（independent set problem）和 漢米爾頓迴圈（Hamiltonian cycle problem）問題上的性質。我們還比較了我們的演算法與最先進的相依量詞布林公式求解器，DQBDD，在解決來自QBFEVAL 2020的競賽測資時的表現。

Succinct representation refers to a way of encoding information, which often leads to an exponential blow-up in complexity. The only known approach for solving succinctly represented problems is to decompress the problem into standard representation, which may discard some additional information implied by the succinct representation.

In this thesis, we focus on two logical frameworks whose satisfiability problems are NEXP-complete: two-variable logic (FO2) and dependency quantified boolean formula (DQBF). FO2 is a decidable fragment of first-order logic that uses at most two variables. DQBF is a generalization of boolean formulae that has applications in the verification and synthesis of hardware and software designs. There has been significant progress in solving DQBF in recent years. We aim to investigate whether solvers for FO$^2$ or DQBF can be used to solve instances derived from succinctly represented problems.

This thesis proposes reductions from succinctly represented NP-complete problems to FO2 and DQBF instances and presents algorithms for solving DQBF. To demonstrate the effectiveness of various approaches for solving succinctly represented problems, this thesis presents two graph series with succinct representations and shows their properties on the independent set problem and the Hamiltonian cycle problem. Additionally, we compare our algorithm with the state-of-the-art DQBF solver, DQBDD, in the Competitive Evaluation of QBF Solvers (QBFEVAL 2020).