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]保持一致。新引入的术语未见其他作者使用,且不与现有术语冲突。