研究室主要的研究成果实体，包括各类约束满足问题的求解器，以及各类运筹优化求解器，均以开源形式发布。关于求解器及软件工具的详细介绍和使用文档，请参考相关源码库或项目主页。
| 名称 | 简介 |
|---|---|
| X-SAT | 电路SAT求解器 |
| PRS | 并行SAT求解器框架 |
| PRS-distributed | 分布式SAT求解器 |
| Relaxed | 混合算法SAT求解器 |
| CCAnr + CP3 | 基于格局检测的局部搜索SAT求解器及与处理器 |
| WalkSAT/SKC (implementation of Cai) | 局部搜索SAT求解器WalkSAT的高效实现 |
| 名称 | 简介 |
|---|---|
| AriParti | 并行SMT变量级划分求解器 |
| Parti-Z3++ | 分布式SMT变量级划分求解器 |
| Z3++ | 基于Z3的衍生求解器，深度融合局部搜索算法和完备算法 |
| hybridSMT | 混合算法SMT求解器 |
| 名称 | 简介 |
|---|---|
| Local-MIP | 高效的混合整数规划MIP的局部搜索求解器，相关论文获CP 2024 最佳论文奖 |
| ParaILP | 整数规划ILP并行局部搜索求解器，深度融合局部搜索和进化算法，相关论文收录于IJCAI 2024 |
| PairLS | MaxSMT的局部搜索求解器，提出了弥补算子，相关论文收录于FM2024 |
| LS-IMP | 多重整数线性规划的局部搜索求解器，相关论文收录于KDD2024 |
| 名称 | 简介 |
|---|---|
| NuWLS | MaxSAT局部搜索求解器，曾用于2022年国际MaxSAT比赛非完备赛道的冠军求解器中。 |
| NuWLS 2.0 | MaxSAT局部搜索求解器，曾用于2023年国际MaxSAT比赛非完备赛道的冠军求解器中。 |
| NuPBO | PBO局部搜索求解器，曾用于2024年国际PB比赛DEC-LIN赛道排名第一与第二的求解器中。 |
| 名称 | 简介 |
|---|---|
| hybridCEC | 组合等价性问题验证器 |
| modelchecker | 模型检查验证器 |