基于CNF结构特征的并行化SAT问题求解策略优化研究

Many important combination, optimization and verification problems in engineering and research domains can be transformed into SAT problems. To improve SAT problem's solving performance is of significant value for both theoretical and practical aspects. The partitioning method divides the original SAT problem into several sub-problems according to its characteristics, and then solves each respectively. The portfolio method selects the most suitable solver and related configurations for the problem according to its features. However, those features are currently generally of statistical information, rather than structural information, which makes the learnt optimization strategy difficult to generalize to arbitrary SAT problems. Some recent work has used the CNF structural features of the SAT problem for satisfiability predication; however, using such CNF structural features for SAT solving performance optimization is still a challenging problem that has not yet been explored. This project aims to extract the complete CNF structural information and related features from the SAT problem and employ adaptive learning methods (most of them belong to deep learning) to solve the optimization problem for both partitioning and portfolio in an integrated manner. The objective is to improve the performance of SAT solving, as well as the accuracy and the robustness of solving strategy learning. It is expected to solve more larger-scale practical problems in a reasonable time.

工程领域和自然科学研究中许多重要的组合、优化、验证问题都可以转化为SAT问题进行求解，研究如何提升SAT问题的求解效率具有重要的理论意义和很强的应用价值。并行分割优化方法将原问题按其特点分割为若干子问题分而治之，多求解配置优化方法根据问题特征选取最合适的求解器及参数。但是，目前这两类优化方法对目标SAT问题的分析都基于其统计特征，而非完整的结构特征，导致其优化能力难以泛化。近期一些工作将SAT问题的CNF结构特征用于可满足性估计；然而，将CNF结构特征用于SAT求解优化，还是一个尚未被探索的挑战性问题。本项目旨在从SAT问题中提取完整的CNF结构信息及其特征，利用深度学习等方法，解决SAT的并行分割和求解配置优化问题，以综合提高SAT求解效率，提升求解策略学习的准确度和鲁棒性，提高对不同类型SAT问题求解优化的泛化能力，以进一步打开相关技术的应用边界，在合理时间内解决更大规模的实际问题。

工程领域和自然科学研究中许多重要的组合、优化、验证问题都可以转化为SAT问题进行求解，研究如何提升SAT问题的求解效率具有重要的理论意义和很强的应用价值。并行分割优化方法将原问题按其特点分割为若干子问题，多求解配置优化方法根据问题特征选取最合适的求解器及参数。针对如何将CNF结构特征用于SAT求解优化这一挑战性问题，本项目从SAT问题中提取完整的CNF结构信息及其特征，利用深度学习等方法，解决SAT的可满足性预测、并行分割和求解配置优化问题。本项目的研究成果提高了SAT求解效率，提升了求解策略学习的准确度和鲁棒性，提高了对不同类型SAT问题求解优化的泛化能力。项目研究成果发表论文7篇，申请专利2项，登记软件著作权4项，研制了验证平台，并在分布式共识协议、软件体系结构设计、人机协同软件设计等领域应用验证。未来拟进一步打开相关技术的应用边界，在合理时间内解决更大规模的实际问题。