Fighting Perebor: New and Improved Algorithms for Formula and QBF Satisfiability
Fighting Perebor: New and Improved Algorithms for Formula and QBF Satisfiability
复制标题
对抗 Perebor：公式和 QBF 满足性的新算法和改进算法
DOI：
10.1109/focs.2010.25
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
R. Santhanam
中科院分区：
文献类型：
--
作者：
R. Santhanam
我们研究了找到令人满意的布尔公式赋值并以比暴力搜索渐近更快的速度测试量化布尔公式（QBF）有效性的可能性。我们的第一个主要结果是一个在 $2^{n - \Omega(n)}$ 时间内运行的简单确定性算法，用于满足 $n$ 中线性大小的公式，其中 $n$ 是公式中变量的数量。该算法扩展到在相同的时间范围内精确计算令人满意的作业的数量。我们的第二个主要结果是一个在 $2^{n - \Omega(n/\log(n))}$ 时间内运行的确定性算法，用于求解 QBF，其中任何变量的出现次数都受常数限制。对于“结构化”的实例，在某种精确意义上，可以修改算法以在$2^{n - \Omega(n)}$ 时间内运行。据我们所知，之前还没有解决这些问题的重要算法。作为用于建立第一个主要结果的技术的副产品，我们证明了每个可通过线性大小公式计算的函数都可以由大小为 $2^{n - \Omega(n)}$ 的决策树表示。因此，我们得到了 Parity 函数的强超线性{\itaverage-case}公式大小下界。
We investigate the possibility of finding satisfying assignments to Boolean formulae and testing validity of quantified Boolean formulae (QBF) asymptotically faster than a brute force search. Our first main result is a simple deterministic algorithm running in time $2^{n - \Omega(n)}$ for satisfiability of formulae of linear size in $n$, where $n$ is the number of variables in the formula. This algorithm extends to exactly counting the number of satisfying assignments, within the same time bound. Our second main result is a deterministic algorithm running in time $2^{n - \Omega(n/\log(n))}$ for solving QBFs in which the number of occurrences of any variable is bounded by a constant. For instances which are ``structured'', in a certain precise sense, the algorithm can be modified to run in time $2^{n - \Omega(n)}$. To the best of our knowledge, no non-trivial algorithms were known for these problems before. As a byproduct of the technique used to establish our first main result, we show that every function computable by linear-size formulae can be represented by decision trees of size $2^{n - \Omega(n)}$. As a consequence, we get strong super linear {\it average-case} formula size lower bounds for the Parity function.