Basically, given an algorithm (properly reduced), can you find a set of inputs that will produce a desired output. It's NP-Complete, which is fun, but why care about this?

Well, using induction, I can analyze source code to find vulns, and, using a SAT solver, confirm that there are some values for set of inputs I control that can cause the vuln code path to actually execute from an external system. Hmmm, sounds like hacking websites doesn't it?

Dug up some old Java code last night to do this I wrote at Tech, and I'm converting it to C# today. Have a feeling I'm going to need this paper again.

The Quest for Efficient Boolean Satisfiability Solver