结合SAT求解器与CAS验证组合猜想 (2016)
本文提出了一种将SAT求解器与计算机代数系统（CAS）相结合的方法，用于自动验证组合数学中的猜想。该方法利用SAT求解器处理布尔约束，同时借助CAS处理代数运算，从而有效解决组合问题中的复杂推理任务。实验结果表明，这种混合方法在多个组合猜想验证中表现出高效性和可扩展性。
背景速读
- 本文介绍了一种将 SAT 求解器（布尔可满足性问题求解器）与计算机代数系统（CAS）相结合的方法，用于自动验证组合数学中的猜想。SAT 求解器擅长处理逻辑约束，CAS 擅长代数运算，两者互补。
- 组合数学研究离散结构（如图、集合、排列）的规律，许多猜想需要大量案例验证，手工难以完成。该论文提出的工具链能自动生成并检查这些案例。
- 作者团队来自剑桥大学等机构，属于形式化验证与符号计算交叉领域。此工作后来影响了更大型的数学验证项目（如使用 SAT 求解器证明“三生素数猜想”相关问题）。
- 对于非专业读者：SAT 即“是否存在一组布尔变量的取值，使得一个巨大的逻辑公式成立？”；CAS 是 Mathematica 或 Maple 这类能做符号化简、解方程的系统。两者结合，等于用逻辑引擎驱动代数计算来验证数学命题。