6
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ 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. $\endgroup$
    – holf
    Commented Mar 24, 2018 at 9:58
  • $\begingroup$ @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) $\endgroup$
    – verifying
    Commented Mar 28, 2018 at 20:52
  • $\begingroup$ Note also that non-deterministic BPs can be unambiguous, in the sense that each assignment leads to a unique clause. $\endgroup$
    – verifying
    Commented Mar 28, 2018 at 20:58

1 Answer 1

Reset to default
1
$\begingroup$

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).

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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