关键词: 多文字可满足, SAT问题, 不满足阈值, 相变点上界, 合取范式

Abstract: The satisfiability problem (SAT) refers to whether there is a set of boolean variable assignments that make at least one literal in each clause of the conjunctive normal form (CNF) formula true. The multi literal SAT problem refers to whether there is a set of boolean variable assignments that make at least two literals in each clause of the CNF formula true. Obviously, this problem is still an NP difficult problem. Defining   as the ratio of the number of clauses in the CNF formula to the number of variables, we study the upper bound  α*  of phase transition point  of the problem. If α strictly exceeds  α*, the multi literal satisfaction problem is almost certainly unsatisfiable. A simple inference of the first moment can be used to prove α*=-ln 2/ln1-(k+1)/2k. α*=1  when k=3. The local maximum technique proposed by Kirousis et al is used to improve the upper bound  α* of phase transition point of the multi literal 3-SAT problem to 0.719 3. Finally, a large amount of data is selected for experimental verification, and the results show that the theoretical results are consistent with the experimental results.

Key words: multi literal satisfiability, satisfiability problem, unsatisfiability threshold, upper bound of phase transition point, CNF