<p>If I understood correctly the question, the so-called <em>Buss-Pudlak</em> game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 <a href="http://math.cas.cz/%7Epudlak/howtolie.ps" rel="nofollow noreferrer">http://math.cas.cz/%7Epudlak/howtolie.ps</a>). The queries are formulas (not just variables). The tree is also completely deterministic. </p>

<p>Other decision trees that correspond to different propositional proof systems exist: e.g., Linear Decision Trees correspond to Res(lin) refutations (cf., <a href="http://www.csc.kth.se/~sokolovd/files/papers/splitting.pdf" rel="nofollow noreferrer">http://www.csc.kth.se/~sokolovd/files/papers/splitting.pdf</a> and <a href="http://cs.rhul.ac.uk/home/tzameret/Res-Lin-Two.pdf" rel="nofollow noreferrer">http://cs.rhul.ac.uk/home/tzameret/Res-Lin-Two.pdf</a>). But there are many other examples (cf., Tonian Pitassi's work on CP-like proof systems).</p>

CC BY-SA 3.0
2018-04-05T10:15:34.687Z
2018-04-05T10:15:34.687Z
Iddo Tzameret
<p>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 <em>deterministic</em> branching program $P$ solving the following search problem: </p>

<p>1) $P$ has one source node and one sink node for each clause $C_i$. </p>

<p>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$. </p>

<p><strong>Question:</strong> 
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 <em>not necessarily deterministic</em> branching program $P$ solving the search problem above? </p>

CC BY-SA 3.0
2018-03-24T09:58:03.190Z
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
CC BY-SA 3.0
2018-03-28T20:52:30.060Z
@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
CC BY-SA 3.0
2018-03-28T20:58:53.397Z
Note also that non-deterministic BPs can be unambiguous, in the sense that each assignment leads to a unique clause.
verifying
<proof-complexity><proof-theory><resolution>
Resolution vs Nondeterministic Search Problems
verifying
# Resolution vs Nondeterministic Search Problems

(Asked by: username_0 on 2018-03-24)

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?

**Tags:** proof-complexity, proof-theory, resolution
> **Comments:**
> **username_1**: 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.  
> **username_0**: @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)  
> **username_0**: Note also that non-deterministic BPs can be unambiguous, in the sense that each assignment leads to a unique clause.  

---

## 1 answers

### Answer by username_2 on 2018-04-05. Score: 1

If I understood correctly the question, the so-called *Buss-Pudlak* game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 <http://math.cas.cz/%7Epudlak/howtolie.ps>). The queries are formulas (not just variables). The tree is also completely deterministic.

Other decision trees that correspond to different propositional proof systems exist: e.g., Linear Decision Trees correspond to Res(lin) refutations (cf., <http://www.csc.kth.se/~sokolovd/files/papers/splitting.pdf> and <http://cs.rhul.ac.uk/home/tzameret/Res-Lin-Two.pdf>). But there are many other examples (cf., Tonian Pitassi's work on CP-like proof systems).


---

