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风格搜索过程配备定制化理论推理。我们实现了该方法，并为有限域上的非线性算术提供了一种新颖且有效的推理原型。