Solving Quantified Boolean Formulas with Few Existential Variables

要約

定量化されたブール式 (QBF) 問題は、一般に PSPACE 完全性の原型とみなされている重要な決定問題です。
AI で中心となる多くの問題 (計画、モデルのチェック、非単調推論など) は一般に NP に含まれておらず、そのような問題に対して QBF がモデリング ツールとしてうまく使用されています。
ただし、QBF のソルバーは最先端の SAT ソルバーほど高度ではないため、QBF が PSPACE 完全問題の汎用モデリング言語になることが妨げられています。
理論的な説明は、QBF (および他の多くの PSPACE 完全問題) には、固定パラメーターの扱いやすさ (FPT) を保証する自然パラメーターが欠如しているということです。
この論文では、この問題に取り組み、単純だが見落とされているパラメータ、つまり存在的に定量化された変数の数を検討します。
この自然なパラメータは文献ではほとんど調査されておらず、QBF 用の FPT アルゴリズムが一般的に不足していることを考えると、驚くべきことに思われるかもしれません。
このパラメータ化を通じて、有界句の長さの結合正規形 (CNF) の QBF インスタンスに適用できる新しい FPT アルゴリズムを開発します。
これを、無制限の文節長の CNF における QBF の W[1] 硬度の結果と、(強い) 指数関数的時間仮説の下での有界アリティの場合のより鋭い下限によって補完します。

要約(オリジナル)

The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters} guaranteeing fixed-parameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google