基于概率推理求解命题逻辑可满足性问题的局部搜索技术研究

The propositional satisfiability problem (SAT) is one of core problems in computer science and artificial intelligence, with particular theoretical significance and many practical applications in domains such as VLSI design, formal verification of software and security protocols. Stochastic local search (SLS) algorithms are so far the most effective incomplete algorithms for large size SAT instances. But, SLS algorithms also have limitations in solving some structured SAT instances from some practical applications. In local search processes for SAT solving, there are rich relationships between clauses and variables under cover. Promisingly, the performance of SLS algorithms will be improved by make full use of these relationships. However, Modern SLS algorithms usually use very simple and deterministic relationships, which are generally obtained from experiences and intuitions or logic resolution. More effective and complex probabilistic relationships between clauses and variables are still not fully exploited for SLS SAT algorithms. This project mainly investigates the following techniques: uncovering and identifying more effective relationships between variables and clauses hidden in local search for SAT problem through appropriate data mining approachs; probabilistically online learning these relationships from local search for a concrete SAT instance solving and constructing a flipping event probabilistic graphical model, and then executing probabilistic inference to get indirect and global probabilistic relationships between variables and clauses (these relationships are closely relevant to the local search process and the SAT instance, which distinguishes our method from factor-graph based Survey Propagation for SAT); designing switch criteria between intensification and diversification during local search by means of enough using these probabilistic relationships. The central issue of this project is to design efficient local search SAT algorithms based on a new type of probabilistic relationships, and then extend these techniques to adapt other combinatorial problem solving.

命题逻辑公式可满足性问题(SAT)是计算机科学与人工智能核心问题之一，在集成电路设计、软件与安全协议形式验证等领域有广泛应用，具有重要理论意义与实用价值。随机局部搜索算法是求解大规模SAT实例最有效的方法，但对于某些应用相关SAT实例，其依然存在局限性。在SAT求解局部搜索过程中，隐藏着丰富的子句与变元间因果关系，充分利用这些关系可有效提高其求解性能。然而，现有算法基于经验与直观提出与利用了一些简单确定性关系，未充分揭示与利用搜索过程中子句与变元间潜在有效的复杂概率关系。本研究旨在利用数据挖掘技术,发现与识别在局部搜索过程中所蕴涵的子句与变元间有效新型关系；在求解过程中学习这些关系，并基于事件概率图模型进行概率推理，获取子句与变元间全局的概率关系；充分应用这些关系指导局部搜索过程，开发智能局部搜索区域动态切换准则。本研究有望设计出高效SAT求解算法，并促进其它组合优化问题求解技术的发展。

命题逻辑公式可满足性问题(SAT)是计算机科学与人工智能核心问题之一，在集成电路设计、软件与安全协议形式验证等领域有广泛应用，具有重要理论意义与实用价值。随机局部搜索算法是求解大规模SAT实例最有效的方法，但对于某些应用相关具有丰富语义与结构的SAT实例，其能力依然不足。项目研究能有效指导SAT局部搜索过程的变元与子句之间状态转换的相互关系、触发机制与概率模型；建立基于概率推理的SAT局部搜索算法与处理策略。. 首先，通过建立SAT局部搜索综合实验环境，采集典型算法搜索行为事件流数据库，利用数据挖掘技术进行关联规则与序列模式挖掘，从而提出了变元与子句间的多元关系与序列关系。进一步，建立了一种基于变元与子句新的概率关系与推理的局部搜索处理框架与软重启策略；提出了有效的搜索过程切换准则，相应求解器在国际SAT大赛中表现出优秀性能。针对搜索过程存在的行为环，提出了行为环的数量特征及基于加强的概率控制策略，使求解效率有显著的改善。另外，在MAXsat问题与大规模图最大团问题的求解算法中，提出了基于推理的优化搜索技术，很好地提高了求解效率。这些研究成果与技术对解决其它组合优化问题具有借鉴作用与重要意义。. 在项目的资助下，项目组在国内外权威期刊与重要国际学术会议上发表学术论文15篇；开发的算法在SAT国际大赛中两次获得第2名的优秀成绩，处于SAT国际研究团队的前列；共培养博士生4名，硕士生9名。