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.
2 Answers
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/.
-
$\begingroup$ (From what I can see, that work is "PCPs for succinct arguments" $\hspace{2.24 in}$ rather than "PCPs in their own right".) $\:$ $\endgroup$– user6973Aug 19, 2013 at 22:20
-
$\begingroup$ succinct arguments are the goal of the work, i am not sure if they develop a general enough PCP encoder for OP's purposes on the way $\endgroup$ Aug 20, 2013 at 4:05
Eli Ben-Sasson's group is working on implementing PCPs. You can e-mail him and ask for their code.