Skip to main content
Conference Proceedings

An upper bound for minimal resolution refutations

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1999) 1584 171-178
DOI: 10.1007/10703163_12
16Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We consider upper bounds for minimal resolution refutations of propositional formulas in CNF. We show that minimal refutations of minimal unsatisfiable formulas over n variables and n+k clauses consist of at most 2k − 1 n 2applications of the resolution rule.

Author supplied keywords

Cite

CITATION STYLE

APA

Büning, H. K. (1999). An upper bound for minimal resolution refutations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1584, pp. 171–178). Springer Verlag. https://doi.org/10.1007/10703163_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free