Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver

Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács

TL;DR

This work addresses SMT solving for non-linear polynomial constraints over finite fields, extending Yices2 with a dedicated MCSat-based finite-field plugin. It introduces an SMT-LIB 2 front-end extension and LibPoly-backed polynomial handling to support $\mathbb{F}_p$ arithmetic, coupled with a zero-decomposition–driven explanation mechanism. The approach interleaves model construction and symbolic reasoning, learning theory lemmas to prune the search space, and is evaluated against cvc5 on finite-field benchmarks showing feasibility and competitive performance in many cases, especially for crafted, structure-rich instances. The modular MCSat framework promises rapid incorporation of further finite-field reasoning techniques, enabling scalable experimentation and extension to additional theories.

Abstract

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.

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver

TL;DR

This work addresses SMT solving for non-linear polynomial constraints over finite fields, extending Yices2 with a dedicated MCSat-based finite-field plugin. It introduces an SMT-LIB 2 front-end extension and LibPoly-backed polynomial handling to support arithmetic, coupled with a zero-decomposition–driven explanation mechanism. The approach interleaves model construction and symbolic reasoning, learning theory lemmas to prune the search space, and is evaluated against cvc5 on finite-field benchmarks showing feasibility and competitive performance in many cases, especially for crafted, structure-rich instances. The modular MCSat framework promises rapid incorporation of further finite-field reasoning techniques, enabling scalable experimentation and extension to additional theories.

Abstract

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.
Paper Structure (17 sections, 1 equation, 3 figures)

This paper contains 17 sections, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. Related Work.
  3. Contributions.
  4. Preliminaries
  5. Yices2 and MCSat.
  6. Usability of SMT Solving in Finite Fields
  7. SMT-LIB 2 Parsing.
  8. Implementation Details
  9. The Implementation of MCSat in Yices2.
  10. The Finite Field MCSat Plugin.
  11. Finite Field Explanations.
  12. Evaluation
  13. Experimental Setup.
  14. Experimental Results.
  15. Summary and Outlook
  16. ...and 2 more sections

Figures (3)

  • Figure 1: Example for an SMT-LIB 2 encoding of a finite field problem $\mathcal{F}_1$.
  • Figure 2: Runtime comparison for benchmarks from hader2023lpar (in seconds, timeout 300s) result: sat o, unsat x; finite field order: 3 (blue), 13 (green), and 211 (orange)
  • Figure 3: Instances solved over time (timeout 300s) by Yices2 ( blue) and cvc5 ( red) from hader2023lpar (left) and ozdemir2023cav (right).