# How to reduce constrained proofs to 0-1 IP

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.

• 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. – Raphael Aug 12 '16 at 9:14

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.