研究室关注的约束求解包括逻辑公式可满足性问题和运筹优化问题：

• 逻辑公式可满足性问题及其优化问题
  • 布尔可满足性（SAT）
  • 可满足性模理论（SMT）
  • 最大可满足性问题（MaxSAT）
  • 最大可满足性模理论（MaxSMT）
  • 优化可满足性模理论（OMT）
• 运筹优化问题
  • 混合整数线性规划（MILP）
  • 混合整数二次规划（MIQP）
  • 伪布尔优化问题/0-1整数规划（PBO）

在对各类约束求解问题深入研究的基础上，我们开发了大量的软件工具，针对不同的问题特征与应用场景对各类问题进行求解。

电子设计自动化（EDA）是研究室重点关注的约束求解应用领域。我们针对EDA研发了相关的形式化验证和测试工具，包括：

• 逻辑等价性验证（LEC）
• 模型检测（MC）
  • 有界模型检测（BMC）
  • PDR证明
• 测试向量生成（ATPG）
• 数字仿真
  • 约束随机数生成

上述工具已经在业界得到应用，其表现也获得相关用户的一致肯定。在EDA形式化验证方面，我们提供的工具可以覆盖千万逻辑门级别组合电路的等价性验证，千万级别（部分电路可达亿级别，如15万逻辑门展开4000步）逻辑门电路设计的有界模型检测差错能力，以及十万逻辑门级别电路设计的模型检测证明能力。

研究室在国际SAT、SMT和MaxSAT等求解器比赛多次获得冠军（包括国内首个SAT冠军，国内首个SMT冠军），在运筹优化榜单MIPLIB刷新了几十个难解实例的求解记录，在国内外EDA比赛和密码分析比赛多次获冠亚军。研究室多次获得国际学术会议论文奖，包括CAV杰出论文奖，SAT最佳论文奖，CP最佳论文奖等（皆为中国首次）。

我们也积极推动形式化验证技术的发展，针对电子设计自动化（EDA），研究定制化求解器和多个形式化验证工具；针对软件验证，研究定制化求解器和相关验证技术，包括组合测试覆盖，符号执行等。我们也针对各种工业场景，基于约束求解技术为多家企业提供解决方案，落地应用包括EDA验证与仿真、云平台故障检测、云平台预配置、电商平台的合约广告流量分配、智慧园区等。