“Split Gröbner Bases for Satisfiability Modulo Finite Fields” by Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett, and Işil Dillig. In Proceedings of the 36^th International Conference on Computer Aided Verification (CAV '24), (Arie Gurfinkel and Vijay Ganesh, eds.), July 2024, pp. 3-25. Montreal, Canada.
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, admits specialized propagation algorithms, e.g., for understanding bitsums. Experiments show that it solves important bitsum-heavy determinism benchmarks far faster than prior solvers, without introducing much overhead for other benchmarks.
BibTeX entry:
@inproceedings{OPB+24,
author = {Alex Ozdemir and Shankara Pailoor and Alp Bassa and Kostas
Ferles and Clark Barrett and I{\c{s}}il Dillig},
editor = {Arie Gurfinkel and Vijay Ganesh},
title = {Split Gr{\"o}bner Bases for Satisfiability Modulo Finite Fields},
booktitle = {Proceedings of the {\it 36^{th}} International Conference
on Computer Aided Verification (CAV '24)},
series = {Lecture Notes in Computer Science},
volume = {14681},
pages = {3--25},
publisher = {Springer},
month = jul,
year = {2024},
doi = {10.1007/978-3-031-65627-9_1},
note = {Montreal, Canada},
url = {http://theory.stanford.edu/~barrett/pubs/OPB+24.pdf}
}
(This webpage was created with bibtex2web.)