Abstract
Solving a system of polynomial equations is one of the hardest problems in mathematics, with
emerging applications in cryptography, software security, and code optimizations. Modern cryptosystems, such as smart contracts, require reasoning techniques over non-linear polynomial systems in finite domains. In this talk we present two MCSat based approaches that address this problem for the use cases of bit-vector reasoning and reasoning over finite fields. We introduce PolySAT, a new bitvector solver that, instead of bit-blasting, performs reasoning on the word level. Constraints in PolySAT are based on polynomials over bitvector variables, i.e., modulo 2^k. PolySAT is being implemented as a theory solver in the SMT solver Z3. Secondly we present our work on solving non-linear polynomial systems over finite fields. We have designed a MCSat style search procedure with two different approaches for explanation functions that rely on algebraic variable elimination techniques.