A satisfiability algorithm for constant depth boolean circuits with unbounded fan-in gates
A satisfiability algorithm for constant depth boolean circuits with unbounded fan-in gates
复制标题
具有无界扇入门的恒定深度布尔电路的可满足性算法
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
W. Matthews
中科院分区：
文献类型：
--
作者：
W. Matthews
我们考虑的问题，有效地枚举满意的分配到AC 0电路。AC 0电路是布尔电路，具有n个输入和它们的否定，一个输出，m = poly（n）总门，和恒定深度，并且由无界扇入AND和OR门组成。我们使用的主要技术工具是一种新的算法方法，用于有效地简化限制类电路。这种方法是基于一个新的扩展版本的Hastad的开关引理。
作为主要结果，我们提出了一个拉斯维加斯算法，该算法以AC 0电路为输入，输出一组限制（分配给输入的子集），这些限制划分{0，1} n，使得在每个限制下电路的输出是常数。该算法以高概率在时间上运行poly（m，n）· 2n（1-µ），并输出最多2n（1-µ）个限制，其中µ = 1/O（lg（m/n）+ d lg d）d −1）。这是最佳的常数在大O枚举的解决方案的限制。这也意味着最有名的算法AC 0电路可满足性和计数满意的分配。
使用类似的技巧，我们也给出了一个算法，用于枚举k-CNF的解决方案，但其中μ=1/ O（k）。以前，具有类似节省μ的算法已知用于找到对k-CNF的单个满意分配，但不用于计数或枚举满意分配。
这些结果对电路下界有一些有趣的应用。我们证明了一个新的界限的相关性的AC 0电路的奇偶校验是最佳的常数，并显示了几个经典的AC 0电路的下界遵循直接从我们的算法。然后，我们使用一个强大的定理，由于威廉姆斯，以显示如何在运行时间的一个小的改进，找到一个单一的满意的分配AC 0电路将意味着NEXP不包含在NC 1。
We consider the problem of efficiently enumerating the satisfying assignments to AC0 circuits. AC0 circuits are Boolean circuits with n inputs and their negations, one output, m = poly(n) total gates, and constant depth, and consist of unbounded fan-in AND and OR gates. The primary technical tool we use is a new algorithmic approach for efficiently simplifying restricted classes of circuits. This approach is based on a new extended version of Hastad's Switching Lemma.
As the main result, we present a Las Vegas algorithm which takes an AC0 circuit as input and outputs a set of restrictions (assignments to subsets of the inputs) which partition {0,1} n such that under each restriction the output of the circuit is constant. With high probability, the algorithm runs in time poly(m,n) · 2n (1–µ) and outputs at most 2n (1–µ) restrictions, where µ = 1/O(lg (m/n) + d lg d)d −1). This is optimal up to the constants in the big- O for enumerating solutions with restrictions. This also implies the best known algorithm for AC0 circuit satisfiability and for counting satisfying assignments.
Using similar techniques, we also give an algorithm for enumerating the solutions to a k-CNF, but where µ=1/ O(k). Previously, algorithms with similar savings µ were known for finding a single satisfying assignment to a k-CNF, but not for counting or enumerating satisfying assignments.
These results have some interesting applications to circuit lower bounds. We prove a new bound on the correlation of AC0 circuits with parity which is optimal up to constants, and show how several classic AC0 circuit lower bounds follow straightforwardly from our algorithm. Then, we use a powerful theorem due to Williams to show how a minor improvement in the running time for finding a single satisfying assignment for an AC0 circuit would imply that NEXP is not contained in NC1.