可满足性问题
本课题组长期活跃于SAT求解的前沿。课题组提出的局部搜索算法CCASat获国内首个国际SAT比赛冠军；以Relaxed为代表的混合求解技术被目前所有主流求解器采用，并获国内首个SAT会议“最佳论文奖”；PRS系列并行求解器获得国内首个SAT比赛并行组的冠军，相关技术被所有主流并行SAT求解器沿用。
在SMT（可满足性模理论）中，算术理论问题是研究中的重要分支之一，主要涉及带有算术约束的逻辑公式的可满足性问题。算术理论一般分为整数算术、实数算术或两者的组合，通常用来描述和验证需要处理数值关系的系统，比如控制系统、数值优化和资源分配等。
运筹优化
最大可满足性问题（MaxSAT）是命题逻辑可满足性问题（SAT）的优化版本，是经典的NP难问题。伪布尔优化问题（PBO）通过引入伪布尔约束，提供了一种更为灵活的表达方式，是一种0-1线性整数规划问题。许多实际问题可以转化为MaxSAT或PBO进行求解，例如规划、调度、软件和硬件验证，以及经典的组合优化问题等。
非线性规划（Nonlinear Programming, NLP）是一类优化问题，其目标函数或约束条件中包含非线性关系。与线性规划相比，非线性规划允许更为复杂的函数形式，因而能够描述更广泛的实际问题。针对非线性规划里的两个子问题，二次规划和多重线性规划。我们设计了通用的局部搜索求解器，提出了针对非线性项的算子以及两阶段切换的操作模式。相比于完备的求解器，我们的求解器能够更高效快速地找到优质解。
混合整数规划（Mixed Integer Programming, MIP），是在满足一些线性约束的限制下，优化一个线性目标函数，其中一些变量要求取整数值，它是运筹学中最基础，应用最广的模型之一，也是经典的NP-Hard问题。MIP求解器在工业生产领域如物流运输，航天调度，芯片设计，生产制造等方面有众多应用，是工业软件中的计算引擎。
EDA形式化验证
实验室在EDA方面主要针对硬件的形式化验证进行研究，特别是针对电路等价性验证、模型检测、测试向量生成等领域进行了领先的研究，并自主研发了相应的形式化验证的工具。在一些来自工业数字电路实例的数据集中，其表现优于开源工具。
