Boolean satisfiability (SAT) solvers are not only routinely used in the formal verification of large industrial problems, but also applied in safety-critical domains such as the railways, avionics, and automotive industries.
A classic counting algorithm, Kirchhoff's theorem gives a formula for finding the number of spanning trees in a simple, connected, undirected graph. I will discuss a simple proof of this theorem, based on elementary linear algebra.
