There has been much discussion about how to combine techniques from computer algebra with SMT solving, which is a form of symbolic computation geared towards program verification. We address the satisfiability of systems of polynomial equations over bit-vectors. Instead of conventional bit-blasting, we exploit word-level inference to translate these systems into non-linear pseudo-boolean constraints. We derive the pseudo-booleans by simulating bit assignments through the addition of (linear) polynomials and applying a strong form of propagation by computing Groebner bases. By handling bit assignments symbolically, the number of Groebner basis calculations, along with the number of assignments, is reduced. The final Groebner basis yields expressions for the bit-vectors in terms of the symbolic bits, together with non-linear pseudo-boolean constraints on the symbolic variables, modulo a power of two. The pseudo-booleans can be solved by translation into classical linear pseudo-boolean constraints (without a modulo) or by encoding them as propositional formulae, for which a novel translation process is described.
Work with Tom Seed and Neil Evans.