Paper detail

On the computational complexity of read once resolution decidability in 2CNF formulas

In this paper, we analyze 2CNF formulas from the perspectives of Read-Once resolution (ROR) refutation schemes. We focus on two types of ROR refutations, viz., variable-once refutation and clause-once refutation. In the former, each variable may be used at most once in the derivation of a refutation, while in the latter, each clause may be used at most once. We show that the problem of checking whether a given 2CNF formula has an ROR refutation under both schemes is NP-complete. This is surprising in light of the fact that there exist polynomial refutation schemes (tree-resolution and DAG-resolution) for 2CNF formulas. On the positive side, we show that 2CNF formulas have copy-complexity 2, which means that any unsatisfiable 2CNF formula has a refutation in which any clause needs to be used at most twice.