有限域算术上的SMT求解
摘要：有限域上的非线性多项式系统被用来模拟密码系统的功能行为，具有系统安全、计算机密码学和后量子密码学等应用。解决多项式系统也是数学中最困难的问题之一。在本文中，我们提出了一种自动推理过程，用于判断有限域上的非线性方程组的可满足性。我们引入了零分解技术，证明有限域上的多项式约束产生有限基解释函数。我们在模型构建可满足性求解中使用这些解释函数，使我们能够在有限域上的SMT求解中为CDCL式的搜索过程提供定制的理论推理。我们实现了我们的方法，并为有限域上的非线性算术提供了一种新颖有效的推理原型。
作者：Thomas Hader, Daniela Kaufmann, Laura Kov''acs
论文ID：2305.00028
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-16