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

TL;DR

This paper investigates the complexity of read-once resolution refutations in 2CNF formulas, revealing NP-completeness for checking such refutations and establishing a bound on clause reuse.

Contribution

It demonstrates that determining read-once resolution refutations in 2CNF formulas is NP-complete and establishes a copy-complexity bound of two for unsatisfiable formulas.

Findings

Checking ROR refutations is NP-complete.

2CNF formulas have copy-complexity 2.

Polynomial refutation schemes exist despite NP-completeness.

Abstract

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.