THE COMPLEXITY OF MODEL CHECKING FOR BOOLEAN FORMULAS

被引：7
|
作者：
Schnoor, Henning [1 ]
机构：
[1] Univ Kiel, Inst Informat, D-24118 Kiel, Germany
来源：
INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE | 2010年 / 21卷 / 03期
关键词：
SATISFIABILITY; CIRCUITS;
D O I：
10.1142/S0129054110007258
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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 reduction
引用
收藏
页码：289 / 309
页数：21
相关论文
共 50 条
  • [1] THE COMPLEXITY OF MODEL CHECKING FOR CIRCUMSCRIPTIVE FORMULAS
    CADOLI, M
    [J]. INFORMATION PROCESSING LETTERS, 1992, 44 (03) : 113 - 118
  • [2] Complexity and probability of some Boolean formulas
    Savicky, P
    [J]. COMBINATORICS PROBABILITY & COMPUTING, 1998, 7 (04): : 451 - 463
  • [3] Complexity of model checking by iterative improvement:: The pseudo-Boolean framework
    Björklund, H
    Sandberg, S
    Vorobyov, S
    [J]. PERSPECTIVES OF SYSTEM INFORMATICS, 2003, 2890 : 381 - 394
  • [4] Complexity of Implementation of Boolean Functions by Real Formulas
    Gashkov, S. B.
    Vegner, Ya. V.
    [J]. MOSCOW UNIVERSITY MATHEMATICS BULLETIN, 2008, 63 (02) : 76 - 78
  • [5] ON GENERIC COMPLEXITY OF THE VALIDITY PROBLEM FOR BOOLEAN FORMULAS
    Rybalov, A. N.
    [J]. PRIKLADNAYA DISKRETNAYA MATEMATIKA, 2016, 32 (02): : 119 - 126
  • [6] Complexity and depth of formulas for symmetric Boolean functions
    Sergeev, I. S.
    [J]. MOSCOW UNIVERSITY MATHEMATICS BULLETIN, 2016, 71 (03) : 127 - 130
  • [7] Model checking with Boolean Satisfiability
    Marques-Silva, Joao
    [J]. JOURNAL OF ALGORITHMS-COGNITION INFORMATICS AND LOGIC, 2008, 63 (1-3): : 3 - 16
  • [8] MODEL CHECKING AND BOOLEAN GRAPHS
    ANDERSEN, HR
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 582 : 1 - 19
  • [9] On Model Checking Boolean BI
    Guo, Heng
    Wang, Hanpin
    Xu, Zhongyuan
    Cao, Yongzhi
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2009, 5771 : 302 - 316
  • [10] MODEL CHECKING AND BOOLEAN GRAPHS
    ANDERSEN, HR
    [J]. THEORETICAL COMPUTER SCIENCE, 1994, 126 (01) : 3 - 30
12345