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

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

项目编号： No.61272014

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 许贵平

作者单位： 华中科技大学

项目金额： 60万元

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

中文关键词： 命题逻辑可满足性问题；随机局部搜索算法；数据挖掘；变元与子句关系；概率推理

英文摘要： 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 fr

英文关键词： Propositional satisfiability problem (SAT)；stochastic local search algorithms；data mining；relationships between variables and clauses；probabilistic inference