Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields
A randomized algorithm is proposed that repeatedly intersects the polynomial system with uniformly random affine linear constraints (hyperplane slices) to progressively reduce the effective dimension of the solution space to address the satisfiability problem in the theory of non-linear arithmetic over finite fields.