The Complexity of Model Checking for Boolean Formulas
The Complexity of Model Checking for Boolean Formulas
复制标题
布尔公式模型检查的复杂性
DOI：
10.1142/s0129054110007258
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Henning Schnoor
中科院分区：
文献类型：
--
作者：
Henning Schnoor
我们检查布尔公式模型检查问题的复杂性，这是以下决策问题：给定一个没有变量的布尔公式，它的计算结果是否为真？我们表明，这个问题的复杂性是由允许构建公式并实现完整分类的连接词的某些闭包属性决定的：公式模型检查问题对于 NC1 来说是完整的，相当于对模 2 进行计数，或者是在非常严格的约简下对于对数时间层次结构的一个级别来说是完整的。
We examine the complexity of the model checking problem for Boolean formulas, which is the following decision problem: Given a Boolean formula without variables, does it evaluate to true? We show that the complexity of this problem is determined by certain closure properties of the connectives allowed to build the formula, and achieve a complete classification: The formula model checking problem is either complete for NC1, equivalent to counting modulo 2, or complete for a level of the logarithmic time hierarchy under very strict reductions.