可满足性模理论（SMT）研究理论谓词的逻辑组合的可满足性,具有强大的表达能力。给定SMT公式，它是否有解？如果有解，解空间的大小如何？这两类问题有重要的科学意义和应用价值。目前SMT求解和解空间大小计算的主要工作都基于DPLL(T)框架。作为SMT求解的完备算法框架，DPLL(T)对于求解难判定理论上的高维SMT公式有很大瓶颈；在SMT解空间大小计算问题上，基于DPLL(T)的算法对维数增加更加敏感，并在解空间呈碎片化分布时效率低下。在本项目中，对于SMT求解问题，我们将结合局部搜索和DPLL(T)的思想，提出一种新的混合求解算法，并研究基于图神经网络的神经-符号求解算法；对于SMT解空间大小计算问题，将重点研究采用哈希函数的近似估算方法，使结果具备理论保证。通过本项目的研究，将显著提高可处理的SMT公式的维数，弥补现有DPLL(T)类算法的局限，并为深度学习与形式化方法的融合提供新思路。

Satisfiability Modulo Theories (SMT) checks the satisfiability of logical formulae with respect to combinations of theory predicates, and is very expressive. Given an SMT formula, is it satisfiable? If the answer is yes, then how large is its solution space? These two problems are not only of scientific significance, but also find important applications in practice. Currently, most works on SMT solving and solution space size computation are based on the DPLL(T) framework. As a complete algorithmic framework for SMT solving, DPLL(T) does not scale well for high dimensional SMT formulae involving theories which are hard to decide; As for computing the size of solution space, DPLL(T)-based algorithm is even more sensitive to the increase of dimensions, and is highly inefficient if the solution space is fragmentized. In this project, for SMT solving, we will develop a new hybrid framework incorporating the ideas of local search and DPLL(T), and investigate the neural-symbolic method based on graph neural networks; For solution space size computation, we will mainly investigate a hash-based approximation algorithm, so as to providing approximation results with theoretical guarantees. Through this project, SMT formulae with much higher dimensions can be processed, and the limitations of DPLL(T)-style algorithms will be complemented. Moreover, new insights can be provided for the merge of deep learning and formal methods.