Gröbner 基理论的新进展及其在形式验证中的应用

我们介绍了环上标准基以及布尔函数框架下布尔 Gröbner 基的基础性工作。这项研究源于我们与电气工程师和计算机科学家在数字电路形式验证问题上的合作。事实上，形式验证问题的代数建模是在字级和位级上开发的。字级模型导出了 $\mathbb{Z}/2^n$ 多项式环中的 Gröbner 基，而位级模型则导出了布尔 Gröbner 基。除了这两种方法的理论基础外，相关算法也已实现。利用这些实现，我们表明特殊的数据结构和对对称性的利用使得 Gröbner 基在与形式验证的最先进工具竞争时具有优势，同时具备系统性和更高灵活性的优点。