可满足性问题的结构特征进展综述

A Review of Structural Characteristics of Satisfiability Problems

可满足性(SAT)问题是人工智能的基础问题,也是NP难问题,在机器学习、模式识别和自然语言处理等领域有着实际应用。然而,随着人工智能发展,越来越多的问题呈现出更为复杂的形态,原有的算法不再适用,需进一步优化或者改进,这对基础研究提出了更高要求。为了研究SAT问题难解的内在本质,需要研究其结构特征,进而找出求解SAT问题的高效算法。近年来备受研究人员关注的相变、树宽、结构熵、DNA折纸术是SAT问题结构特征的4种常用度量模型。为了理清关于SAT问题结构特征的研究进展,基于上述4种度量模型,对SAT问题的结构特征进行了综述,指出了SAT问题结构特征研究所面临的挑战及未来的方向。在SAT问题求解中相变分析、树分解算法、结构熵及DNA折纸术等方面虽已取得一定的研究成果,但在相变点精确上界的求解、结构度量模型指导SAT求解器设计,以及树分解算法效率的提高等方面仍待突破,这将成为未来关于SAT问题结构特征研究的重点。

Satisfiability(SAT)problem is the basic problem of artificial intelligence,which is also a hard problem of NP.It has practical applications in machine learning,pattern recognition and natural language processing.However,with the development of artificial intelligence,more and more complex problems popped up.The original algorithms were no longer applicable and need to be further optimized or improved,which put forward higher requirements for basic research.In order to study the inherent nature of the difficult SAT problem,the structural characteristics of the problem were studied,and then the efficient algorithm to solve the SAT problem were found out.Phase transition,tree width,structural entropy,and DNA origami were four metric models for studying the structural characteristics of SAT problems,which attracted the attention of researchers in recent years.In order to clarify the research progress on the structural characteristics of SAT problems,based on the above four measurement models,the structural characteristics of SAT problems were summarized,and the challenges and future directions of the research on structural characteristics of SAT problems were pointed out.Although some research achievements were made in phase change analysis,tree decomposition algorithm,structural entropy and DNA origami in solving SAT problems,breakthroughs are still needed in solving the accurate upper bound of phase change points,guiding the design of SAT solvers by structural metric model,and improving the efficiency of tree decomposition algorithm,which will become the focus of future research on structural characteristics of SAT problems.