Question: Does anyone know of interesting applications of [Gröbner bases](http://en.wikipedia.org/wiki/Gr%C3%B6bner_basis) to theoretical computer science?

Gröbner bases are used to solve multi-variate polynomial equations, an NP-hard problem in general. I was wondering whether some tractable special cases were used to provide efficient algorithms/constructions/proofs in TCS or TCS-related areas (combinatorics, coding theory).

Answer: 
Gröbner basis computation, while EXPSPACE-complete in general, are in PSPACE over Boolean rings. This has applications in model-checking to replace BDDs: Quoc-Nam Tran, "A PSPACE Algorithm for Groebner Bases Computation in Boolean Rings", Proc. WASET, Vol. 35, Nov. 2008, ISSN 2070-3740

**[NOTE]** The result stating that Groebner basis computation is in PSPACE over Boolean rings seems wrong, see Mark van Hoeij, **Gröbner basis in Boolean rings is not P-SPACE**, arXiv:[1502.07220](http://arxiv.org/abs/1502.07220), 2015.

**[NOTE]** The claim that the result stating that Groebner basis computation is in PSPACE over Boolean rings seems wrong, is wrong. The author confuses PSPACE-computability with having a polynomial size. A PSPACE function may well have exponentially long output.
I used a Gröbner basis to help find a short proof of a new dichotomy theorem for #CSP problems over 3-regular graphs with a single binary constraint function that has complex weights ([arXiv version](http://arxiv.org/abs/1108.3383)).

There is natural equivalence relation over the set of constraint functions, namely, $f \sim g$ if $\#\operatorname{CSP}(f) = \#\operatorname{CSP}(g)$ for all possible instance graphs. For 3-regular graphs, there are fewer equivalence classes than would otherwise exist over all possible graphs. Since a dichotomy theorem only needs to prove the complexity of one constrain function in each equivalence class, this leads to a shorter proof.

The Gröbner basis is used to convert from the initial four variables needed to define a binary function to six "symmetrized variables" that are invariant in each equivalence class (see section D of the paper linked above). However, the Gröbner basis is not mentioned in the paper since its only purpose was the automated transformation from the initial four variables to the six symmetrized variables in various polynomials (which was preformed by [Mathematica's GroebnerBasis](http://reference.wolfram.com/mathematica/ref/GroebnerBasis.html)).