1
$\begingroup$

Consider the following problem:

Can $X$ be proven in fewer than $Y$ steps, from axioms $Z$, with finitely many transition rules $\tau$?

This lies in $NP$, since if I supply a proof $M$, and individual steps can checked against the list of possible transitions $\tau$ in polynomial time, then $M$ can be checked for length $<=Y$ in linaer time, and verified for correctness in $Y*O(n^{O(1)})$

What isn't clear is how to reduce this generic "finite resource" automated theorem proving problem, to 3-SAT.

Obviously it should be reducible since $3-SAT$ is NP Complete but it's not clear how to do that.

$\endgroup$
  • $\begingroup$ I don't see why proofs $M$ have to be polynomial in the length of the input $\langle X, Y, Z, \tau \rangle$. Hence, I'm not convinced that this problem is in NP. $\endgroup$ – Raphael Aug 12 '16 at 9:14
1
$\begingroup$

If your problem is truly in NP, the reduction follows immediately from the Cook-Levin theorem. You described how to build a verifier for your problem. The proof of the Cook-Levin theorem shows how to turn that into a 3SAT instance. Basically, the variables of the 3SAT formulas are the intermediate states of the verifier, and the formula itself says that each pair of consecutive states are consistent and that the verifier ends up accepting.

I am not persuaded by your proof that it is in NP. Your proof would be fine if $Y$ is provided on the input in unary, but not if it is provided in binary -- in the latter case, the length of the proof is exponential in the size of the input, so your proposed verifier doesn't run in polynomial time. If the problem is not in NP, there is no (polynomial-time) reduction to 3SAT.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.