Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields

Abstract

We address the satisfiability problem in the theory of non-linear arithmetic over finite fields. This problem is of significant practical interest, particularly motivated by verification tasks from cryptography, coding theory, and smart contracts. While existing methods provide completeness, they can become impractical when the solution set has non-zero dimension and brute-force enumeration is infeasible for the field sizes that arise in practice. We propose a randomized algorithm that repeatedly intersects the polynomial system with uniformly random affine linear constraints (hyperplane slices) to progressively reduce the effective dimension of the solution space. Once a zero-dimensional system is obtained, we invoke existing techniques from finite field SMT solving to obtain a model. If the input is satisfiable, we find a witness with high probability, with success amplified by independent trials. We formalize the dimension-drop intuition via probabilistic slicing arguments over finite fields and show how our method fits naturally into an SMT workflow. We implemented our algorithm as an improvement to the finite field reasoning engine of the CVC5 SMT solver. We provide extensive experimental results demonstrating significant gains in scalability when using our work compared to existing methods implemented in CVC5.