Finding read-once resolution refutations in systems of 2CNF clauses. (English) Zbl 1435.03086
Summary: 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 is NP-complete, under both schemes. This is surprising, in light of the fact that there exist polynomial time 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. The study of resolution refutation schemes is a sub-field of proof complexity, which has received a lot of attention in the literature.
MSC:
| 03F20 | Complexity of proofs |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Aharoni, R.; Linial, N., Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas, J. Combin. Theory Ser. A, 43, 196-204 (1986) · Zbl 0611.05045 |
| [2] | Beame, P.; Pitassi, T., Simplified and improved resolution lower bounds, (37th Annual Symposium on Foundations of Computer Science (1996), IEEE), 274-282 |
| [3] | Beame, P.; Pitassi, T., Propositional proof complexity: past, present, future, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS, 65, 66-89 (1998) · Zbl 0908.68164 |
| [4] | Buss, P.; Pitassi, T., Resolution and the weak pigeonhole principle, (CSL: 11th Workshop on Computer Science Logic. CSL: 11th Workshop on Computer Science Logic, LNCS (1997), Springer-Verlag) |
| [5] | Cook, S.; Reckhow, R., Time bounded random access machines, J. Comput. System Sci., 7, 4, 354-375 (1973) · Zbl 0284.68038 |
| [6] | Davidov, G.; Davydova, I.; Kleine Büning, H., An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, Ann. Math. Artif. Intell., 23, 229-245 (1998) · Zbl 0913.68090 |
| [7] | Even, S.; Itai, A.; Shamir, A., On the complexity of timetable and multicommodity flow problems, SIAM J. Comput., 5, 691-703 (1976) · Zbl 0358.90021 |
| [8] | Fleischer, H.; Kullmann, O.; Szeider, S., Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference, Theoret. Comput. Sci., 289, 1, 503-516 (2002) · Zbl 1061.68072 |
| [9] | Fortune, S.; Hopcroft, J. E.; Wyllie, J., The directed subgraph homeomorphism problem, Theoret. Comput. Sci., 10, 2, 111-121 (1980) · Zbl 0419.05028 |
| [10] | Haken, A., The intractability of resolution, Theoret. Comput. Sci., 39, 2-3, 297-308 (1985) · Zbl 0586.03010 |
| [11] | Iwama, K.; Miyano, E., Intractability of read-once resolution, (Proceedings Structure in Complexity Theory. Proceedings Structure in Complexity Theory, 10th Annual Conference (IEEE) (1995)), 29-36 |
| [12] | Kleine Büning, H.; Zhao, X., The complexity of read-once resolution, Ann. Math. Artif. Intell., 36, 4, 419-435 (2002) · Zbl 1015.68081 |
| [13] | Kleine Büning, H.; Zhao, X., On the structure of some classes of minimal unsatisfiable formulas, Discrete Appl. Math., 130, 185-207 (2003) · Zbl 1029.68078 |
| [14] | Kleine Büning, H.; Zhao, X., Read-once unit resolution, (Theory and Applications of Satisfiability Testing, vol. 2919 (2004)), 356-369 · Zbl 1204.03022 |
| [15] | Papadimitriou, C. H.; Wolfe, D., The complexity of facets resolved, J. Comput. System Sci., 37, 2-13 (1988) · Zbl 0655.68041 |
| [16] | Papadimitriou, C. H., Computational Complexity (1994), Addison-Wesley: Addison-Wesley New York · Zbl 0833.68049 |
| [17] | Robinson, J., A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41 (1965) · Zbl 0139.12303 |
| [18] | A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning.; A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning. · Zbl 1178.03001 |
| [19] | Subramani, K., Optimal length tree-like resolution refutations for 2sat formulas, ACM Trans. Comput. Log., 5, 2, 316-320 (2004) · Zbl 1367.68114 |
| [20] | Szeider, S., NP-completeness of refutability by literal-once resolution. Automated reasoning, (First International Joint Conference (2001)), 168-181 · Zbl 0988.03020 |
| [21] | Urquhart, A., The complexity of propositional proofs, Bull. Symbolic Logic, 1, 4, 425-467 (1995) · Zbl 0845.03025 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
