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.
This research was supported in part by the National Science Foundation through Award CCF-1305054.
This work was supported by the Air Force Research Laboratory under US Air Force contract FA8750-16-3–6003. The views expressed are those of the authors and do not reflect the official policy or position of the Department of Defense or the U.S. Government.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Aharoni, R., Linial, N.: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. J. Combin. Theor. Ser. A 43, 196–204 (1986)
Davidov, G., Davydova, I., Kleine Büning, H.: An efficient algorithm for the minimal unsatisability problem for a subclass of CNF. Ann. Math. Artif. Intell. 23, 229–245 (1998)
Fleischer, H., Kullmann, O., Szeider, S.: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theor. Comput. Sci. 289(1), 503–516 (2002)
Fortune, S., Hopcroft, J.E., Wyllie, J.: The directed subgraph homeomorphism problem. Theor. Comput. Sci. 10(2), 111–121 (1980)
Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory, pp. 29–36. IEEE (1995)
Kleine Büning, H., Zhao, X.: The complexity of read-once resolution. Ann. Math. Artif. Intell. 36(4), 419–435 (2002)
Kleine Büning, H., Zhao, X.: On the structure of some classes of minimal unsatisfiable formulas. Discrete Appl. Math. 130, 185–207 (2003)
Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci. 37, 2–13 (1988)
Even, S., Itai, A., Shamir, A.: On the complexity of timetable and multicommodity flow problems. SIAM J. Comput. 5, 691–703 (1976)
Beame, P., Pitassi, T.: Propositional proof complexity: past, present, future. Bull. EATCS 65, 66–89 (1998)
Robinson, J.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Bachmair, L., Ganzinger, H., McAllester, D., Lynch, C.: Bachmair, L., Ganzinger, H., McAllester, D., Lynch, C.: Chapter 2 - Resolution theorem proving. Handbook of Automated Reasoning, Issue. 1, pp. 19–99 (2001)
Szeider, S.: NP-Completeness of refutability by literal-once resolution. In: Automated Reasoning: First International Joint Conference, pp. 168–181 (2001)
Urquhart, A.: The complexity of propositional proofs. Bull. Symbolic Logic 1(4), 425–467 (1995)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Kleine Büning, H., Wojciechowski, P., Subramani, K. (2017). On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas. In: Gopal, T., Jäger , G., Steila, S. (eds) Theory and Applications of Models of Computation. TAMC 2017. Lecture Notes in Computer Science(), vol 10185. Springer, Cham. https://doi.org/10.1007/978-3-319-55911-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-55911-7_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-55910-0
Online ISBN: 978-3-319-55911-7
eBook Packages: Computer ScienceComputer Science (R0)