Split Gröbner Bases for Satisfiability Modulo Finite Fields

ePrint Report: Split Gröbner Bases for Satisfiability Modulo Finite Fields

Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett, Işil Dillig

Satisfiability modulo finite fields enables automated verification for cryptosystems. Unfortunately, previous solvers scale poorly for even some simple systems of field equations, in part because they build a full Gröbner basis (GB) for the system. We propose a new solver that uses multiple, simpler GBs instead of one full GB. Our solver, implemented within the cvc5 SMT solver, …

alex automated build eprint report report scale simple systems verification