Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic circuits and, more generally, systems of polynomial equations in a large prime field (commonly ranging from 64-bit to 256-bit values). An increasing interest to apply formal verification techniques to ensure soundness and completeness properties of ZKP protocols has shown the need of developing powerful SMT solvers able to handle such constraint systems. In this paper we consider the problem of deciding the satisfiability of existentially quantified first-order formulas defined over polynomial equations on a prime field. We present a new DPLL($T$)-based approach in which the theory solver orchestrates several modules with different trade-offs between completeness and efficiency. We have implemented the proposed techniques in a prototype that already shows better results than existing state-of-the-art tools on both benchmarks from the domain of ZKP compiler correctness and new benchmarks coming from the verification of arithmetic circuits for ZKPs. \keywords{SMT \and Finite field \and Polynomials \and Zero-Knowledge Proofs.

翻译：零知识证明（ZKPs）是一项新兴技术，已成为在满足区块链透明性要求的同时高效提供安全性与隐私性的解决方案。ZKPs通常通过算术电路、更广泛而言通过大素数域（通常为64位至256位数值）上的多项式方程组进行表述。随着应用形式化验证技术确保ZKP协议完备性与可靠性的需求日益增长，开发能够处理此类约束系统的强大SMT求解器变得尤为必要。本文研究了判定素数域上多项式方程定义的存在量化一阶公式可满足性的问题。我们提出了一种基于DPLL($T$)的新型方法，其中理论求解器对多个在完备性与效率间存在不同权衡的模块进行编排。我们在原型系统中实现了所提出的技术，在ZKP编译器正确性基准测试和ZKP算术电路验证新基准测试中，均展现出优于现有最先进工具的结果。 \keywords{SMT \and 有限域 \and 多项式 \and 零知识证明}