The research in this article aims to find conditions of an algorithmic nature that are necessary and sufficient to transform any Boolean function in conjunctive normal form into a specific form that guarantees the satisfiability of this function. To find such conditions, we use the concept of a special covering of a set introduced in [13], and investigate the connection between this concept and the notion of satisfiability of Boolean functions. As shown, the problem of existence of a special covering for a set is equivalent to the Boolean satisfiability problem. Thus, an important result is the proof of the existence of necessary and sufficient conditions that make it possible to find out if there is a special covering for the set under the special decomposition. This result allows us to formulate the necessary and sufficient algorithmic conditions for Boolean satisfiability, considering the function in conjunctive normal form as a set of clauses. In parallel, as a result of the aforementioned algorithmic procedure, we obtain the values of the variables that ensure the satisfiability of this function. The terminology used related to graph theory, set theory, Boolean functions and complexity theory is consistent with the terminology in [1], [2], [3], [4]. The newly introduced terms are not found in use by other authors and do not contradict to other terms.
翻译:本文旨在寻找算法性质的充要条件,使得任意合取范式布尔函数可转化为保证其可满足性的特定形式。为寻找此类条件,我们采用了文献[13]中引入的集合特殊覆盖概念,并探究该概念与布尔函数可满足性概念之间的关联。研究表明,集合特殊覆盖的存在性问题等价于布尔可满足性问题。因此,一个重要成果是证明了在特殊分解下存在充要条件以判定集合是否具有特殊覆盖。该结论使我们能够将合取范式布尔函数视为子句集,从而提出布尔可满足性的算法化充要条件。与此同时,通过上述算法过程,我们还能获得确保该函数可满足性的变量赋值。本文使用的图论、集合论、布尔函数及复杂度理论相关术语与文献[1][2][3][4]保持一致,新引入的术语均未见于其他文献,且与其他术语不存在冲突。