2024/02/27 by Thomas Häder, Hader, Thomas, Daniela Kaufmann +7 · 1 citation
Computer Science · #Distributed and Parallel Computing Systems #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2402.17927
openalex publication_date 2024/02/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2's frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.