- 學位論文
存在性二階布林運算式的隨機可驗證系統和其不可估計性
A PCP Protocol for Existential SOQBF and the Inapproximability Result
摘要
隨機可驗證系統 (probabilistic checkable proof) 是一種證明系統，讓驗證證明的驗證者只需隨機查看部份證明內容即可高機率確認其正確性。事實上，許多被認為困難的問題包含非確定性多項式時間計算 (non-deterministic polynomial-time computation) 和 非 確 定 性 指 數 時 間 計 算 (non-deterministic exponential-time computation) 都能使用此種證明系統，並且驗證者只須隨機查看證明中常數個位元的內容即可高機率確認證明的正確性。此結果被稱為隨機可驗證系統理論 (the PCP theorem)，在資訊理論和現實世界中都有許多應用。其中一個應用領域為可驗證計算 (verifiable computation)，此領域的研究者嘗試建立一套機制，使得人們能快速驗證其他人是否正確執行某項電腦計算。過去十年來，研究者提出各種不同的方法來實現可驗證計算，不過他們的方法和討論都集中於（非）確定性多項式時間。近幾年，研究者開始探討超過多項式時間或空間的（非）確定性計算。本論文將嘗試使用隨機可驗證系統建構非確定性指數時間計算的可驗證計算。準確來說，本論文先利用存在性二階布林運算式 (existential second-order boolean formula) 來精簡地表示任何非確定性指數時間計算的計算表，再為存在性二階布林運算式設計一隨機可驗證系統。另外，本論文也證明估計存在性二階布林運算式滿足與否為非確定性指數時間完備問題。
並列摘要
Probabilistic checkable proof (PCP) is a type of proof format that could be verified with high probability by only looking at a small portion of the proof. It turns out that problems in NP and even in NEXP have PCP proofs that could be verified in polynomial time by only looking at a constant number of bits in the proof. The result is known as the PCP theorem and has both practical and theoretical significance. One of its practical applications lies in the field of verifiable computation, which aims to provide a scheme for one to efficiently verify if a computation is carried out correctly by others. There are many different approaches in the field while most of the work are dedicated to deterministic/non-deterministic computation in polynomial time. Recently, some researchers investigate the possibility of constructing schemes for deterministic/non-deterministic computation beyond polynomial time and space. In the thesis, we try to construct a scheme for non-deterministic computation in exponential time based on PCP proofs. Specifically, we succinctly encode any non-deterministic exponential computation tableau by a logic known as ∃SOQBF and construct a PCP proofs for ∃SOQBF. In addition, we also show that it is NEXP-hard to approximate the satisfiability of ∃SOQBF within any constant factor.