A CNF formula hierarchy over the hypercube

作者: Stefan Porschen

DOI: 10.1007/978-3-540-76928-6_25

关键词: Boolean satisfiability problemMathematicsDiscrete mathematicsHierarchy (mathematics)Propositional variableConjunctive normal formSatisfiabilityCombinatoricsMaximum satisfiability problemHypercubePropositional formula

摘要: We study the first level of a conjunctive normal form (CNF) formula hierarchy with respect to propositional satisfiability problem (SAT). This is defined over base that we call hypercube (formula). Such simply consists all 2n possible n-clauses given set n Boolean variables. The are 1-hyperjoins, meaning arbitrary hypercubes joined together via taking from each many clauses for joining, i.e., set-union, such chosen clause occurs in at most one new 1-hyperjoin. prove 1-hyperjoins can efficiently be recognized and solved w.r.t. SAT. To end introduce simple closure concept on variables formula.

参考文章(7)
Endre Boros, Peter L. Hammer, Xiaorong Sun, Recognition of q -Horn formulae in linear time Discrete Applied Mathematics. ,vol. 55, pp. 1- 13 ,(1994) , 10.1016/0166-218X(94)90033-7
B. Monien, E. Speckenmeyer, Solving satisfiability in less than 2n steps Discrete Applied Mathematics. ,vol. 10, pp. 287- 295 ,(1985) , 10.1016/0166-218X(85)90050-2
Bengt Aspvall, Michael F. Plass, Robert Endre Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas☆ Information Processing Letters. ,vol. 8, pp. 121- 123 ,(1979) , 10.1016/0020-0190(79)90002-4
Stephen A. Cook, The complexity of theorem-proving procedures symposium on the theory of computing. pp. 151- 158 ,(1971) , 10.1145/800157.805047
John Franco, Allen Van Gelder, A perspective on certain polynomial-time solvable classes of satisfiability Discrete Applied Mathematics. ,vol. 125, pp. 177- 214 ,(2003) , 10.1016/S0166-218X(01)00358-4
E. Boros, Y. Crama, P. L. Hammer, Polynomial-time inference of all valid implications for Horn and related formulae Annals of Mathematics and Artificial Intelligence. ,vol. 1, pp. 21- 32 ,(1990) , 10.1007/BF01531068
Rodney G. Downey, M. R. Fellows, Parameterized Complexity ,(1998)