1

I understand that in general, non-linear integer arithmetic is undecidable. However, this is not the case for the arithmetic of finite fields mod p, as in particular this can be reduced to a SAT problem over finite bit vectors. The reduction to SAT is however, it seems, somewhat inefficient for large primes p (this is Z3's default behaviour).

Is there a more efficient way of modelling arithmetic operations in Z3 over such a finite field? Perhaps performance improvements can be made over Z3's default strategy from the knowledge that all arithmetic operations are over the same finite field?

Julian Sutherland
  • 21
  • 2
  • While it's true you can reduce it to finite BVs, the resulting bit-vectors are typically too large for practical values of `p`. (384 bits or larger for modern ECC applications.) This makes the problem decidable in theory, but in practice it's still too large for a SAT/SMT solver to deal with effectively. – alias Apr 03 '22 at 23:20

0 Answers0