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).
CITATION STYLE
Ozdemir, A., Kremer, G., Tinelli, C., & Barrett, C. (2023). Satisfiability Modulo Finite Fields. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13965 LNCS, pp. 163–186). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-37703-7_8
Mendeley helps you to discover research relevant for your work.