作者: Stefan Porschen
DOI: 10.1007/978-3-540-76928-6_25
关键词: Boolean satisfiability problem 、 Mathematics 、 Discrete mathematics 、 Hierarchy (mathematics) 、 Propositional variable 、 Conjunctive normal form 、 Satisfiability 、 Combinatorics 、 Maximum satisfiability problem 、 Hypercube 、 Propositional 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.