We all know the PCP Theorem. Is there any software package availalbe taking a CNF in e.g. DIMACS format as input, and producing a PCP encoding in the same format as output? It might be interesting to run existing SAT solvers on such encoded instances and compare the performance relative to plain instances.
There has been some recent effort to make PCPs practical for use in verifying outsourced computation. Check the work by this UT Austin group for example: http://www.cs.utexas.edu/pepper/.