# Resolution vs Nondeterministic Search Problems

It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can be translated in polynomial time (in the size of $\Pi$) into a deterministic branching program $P$ solving the following search problem:

1) $P$ has one source node and one sink node for each clause $C_i$.

2) For each assingment $\alpha:X\rightarrow \{0,1\}$ there is a consistent path in $P$ from the source node to some sink node associated with a clause that is falsified by $\alpha$.

Question: Is there a proof system strictly stronger than resolution where each proof $\Pi$ can be translated in polynomial time (in the size of $\Pi$) into a not necessarily deterministic branching program $P$ solving the search problem above?

• If I am giving you a CNF $F$ and a non-deterministic BP $P$ with clauses at the sinks, how would you check that $P$ is indeed a proof that $F$ is unsatisfiable? Looks hard: you can construct a read once BP $B_C$ for each clause $C$ computing $\neg C$ with $C$ as its sink and then add a non-deterministic node branching all $B_C$ together. – holf Mar 24 '18 at 9:58
• @holf, your argument can be equally applied to deterministic read-$m$ branching programs: For each clause $C_i$ construct a read-once BP $B_{C_i}$ computing $\neg C_i$, and then apply these BPs sequentially. Given an assignment $\alpha$, output the $C_i$ if $B_{C_i}$ is the first BP accepting $\alpha$... The question is not about determining if a given BP is a proof of unsatisfiability. Either in the deterministic or in the non-deterministic case this is guaranteed by the fact that the BP was obtained from a valid refutation. (I have edited the question to make it clearer) – verifying Mar 28 '18 at 20:52
• Note also that non-deterministic BPs can be unambiguous, in the sense that each assignment leads to a unique clause. – verifying Mar 28 '18 at 20:58