On the computational complexity of read once resolution decidability in 2CNF formulas
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.
Cite
@article{arxiv.1610.04523,
title = {On the computational complexity of read once resolution decidability in 2CNF formulas},
author = {Hans Kleine Büning and Piotr Wojciechowski and K. Subramani},
journal= {arXiv preprint arXiv:1610.04523},
year = {2016}
}
Comments
14 pages, 3 figures