Solving non-linear Boolean equation systems by variable elimination

In this paper we study Boolean equation systems, and how to eliminate variables from them while bounding the degree of polynomials produced. A procedure for variable elimination is introduced, and we relate the techniques to Gröbner bases and XL methods. We prove that by increasing the degree of the polynomials in the system by one for each variable eliminated, we preserve the solution space, provided that the system satisfies a particular condition. We then estimate how many variables we need to eliminate in order to solve the resulting system by re-linearization, and show that we get complexities lower than the trivial brute-force O(2n) when the system is overdetermined.