Research On Message Propagation Algorithm Of The Random Multi-literal Satisfying Problem

The constraint satisfaction problem(CSP)is a hot research problem in many disciplines such as computer science,mathematics and physics.The satisfiability(SAT)problem of proposition formula is the most basic CSP.Given a conjunctive normal form(CNF)formula F,the SAT question refers to whether there is a set of Boolean variable assignment such that at least one literal in each clause of the CNF formula is true.However,the constraint satisfaction problems in life tend to be more complex than SAT problems.Various NP-hard problems are often not encoded by standard SAT instance.So SAT problems with multiple literals per clause need to be studied.The random multi-literal SAT problem(MLSAT)refers to whether there is a set of variable assignment such that at least two literals in each clause of the CNF instance are true.The message propagation algorithm is the most effective algorithm for solving the SAT problem at present.Therefore,this paper design message propagation algorithm for solving the MLSAT problem,and studies the upper bound for the MLSAT problem threshold.Specifically,the research contents are as follows:(1)The CNF random instance generation model is introduced to design a belief propagation(BP)algorithm suitable for solving the MLSAT problem,we get the variable marginal probability.BP heuristic extraction algorithm and BP random walk heuristic extraction algorithm are presented,and their convergence is analyzed.Finally,we analyze the BP algorithm principle,a large amount of data is generated by random instance generation model for experimental verification.The results show that the performance of this algorithm is better than traditional heuristic algorithm.(2)Define?as the ratio of the number of clauses to the number of variables in the CNF formula,we study the upper bound?_s(k)for the MLSAT problem threshold.If?>?_s(k),then the probability of MLSAT being satisfiable converges to 0 as n approaches infinity.The CNF random instance generation model is introduced.Based on the first moment method and the local maximum principle,the upper bound accuracy for the MLSAT problem threshold is improved by using a single flip and two flips.A large amount of data is selected for experimental verification,the results show that the theoretical results are consistent with the experimental results.