Satisfiability Modulo Finite Fields
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett · Lecture notes in computer science · 2023
Abstract We study satisfiability modulo the theory of finite fields and give a decision procedure for this theory. We implement our procedure for prime fields inside the cvc5 SMT solver. Using this theory, we construct SMT queries that encode translation validation for various zero knowledge proof compilers applied to Boolean computations. We evaluate our procedure on these benchmarks. Our experiments show that our implementation is superior to previous approaches (which encode field arithmetic using integers or bit-vectors).