Non-linear polynomial systems over finite fields are used to model functional behavior of cryptosystems, with applications in system security, computer cryptography, and post-quantum cryptography. Solving polynomial systems is also one of the most difficult problems in mathematics. In this paper, we propose an automated reasoning procedure for deciding the satisfiability of a system of non-linear equations over finite fields. We introduce zero decomposition techniques to prove that polynomial constraints over finite fields yield finite basis explanation functions. We use these explanation functions in model constructing satisfiability solving, allowing us to equip a CDCL-style search procedure with tailored theory reasoning in SMT solving over finite fields. We implemented our approach and provide a novel and effective reasoning prototype for non-linear arithmetic over finite fields.

翻译：有限域上的非线性多项式系统被用于建模密码系统的功能行为，其应用涵盖系统安全、计算机密码学及后量子密码学。多项式系统的求解也是数学中最困难的问题之一。本文提出了一种自动推理过程，用于判定有限域上非线性方程组可满足性问题。我们引入零分解技术，证明有限域上的多项式约束可产生有限基解释函数。在模型构造可满足性求解中运用这些解释函数，使得我们能够在有限域的SMT求解过程中，为CDCL风格的搜索过程配备定制化的理论推理。我们实现了该方法，并构建了一个针对有限域非线性算术的全新高效推理原型系统。