SAT-SMT

本课题组长期活跃于SAT求解的前沿。课题组提出的局部搜索算法CCASat获国内首个国际SAT比赛冠军；以Relaxed为代表的混合求解技术被目前所有主流求解器采用，并获国内首个SAT会议“最佳论文奖”；PRS系列并行求解器获得国内首个SAT比赛并行组的冠军，相关技术被所有主流并行SAT求解器沿用。

可满足性模理论（SMT）问题在串行的算法与硬件平台上达到了性能的瓶颈。我们致力于在多核并行以及分布式平台上进一步提升SMT求解算法的性能。

在SMT（可满足性模理论）中，算术理论问题是研究中的重要分支之一，主要涉及带有算术约束的逻辑公式的可满足性问题。算术理论一般分为整数算术、实数算术或两者的组合，通常用来描述和验证需要处理数值关系的系统，比如控制系统、数值优化和资源分配等。