An upper bound for minimal resolution refutations

DOI10.1007/10703163_12MaRDI QIDQ4263797zbMATH OpenFDO

Authors Hans Kleine Büning

Publication date 22 September 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10703163_12

zbMATH Keywords

conjunctive normal formlength of proofsminimal unsatisfiable formulasupper bounds for minimal resolution refutations of propositional formulas

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• Minimally unsatisfiable CNF formulas
• An optimal lower bound for resolution with 2-conjunctions
• Narrow proofs may be maximally long
• Space bounds for resolution

Cited in

(12)

• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Homomorphisms of conjunctive normal forms.
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On subclasses of minimal unsatisfiable formulas
• Investigations on autark assignments
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Lower bounds and recursive methods for the problem of adjudicating conflicting claims
• On minimal unsatisfiability and time-space trade-offs for k-DNF resolution
• The Lovász Local Lemma and Satisfiability
• NP-completeness of refutability by literal-once resolution
• An optimal lower bound for resolution with 2-conjunctions
• An upper bound for the circuit complexity of existentially quantified Boolean formulas

This page was built for publication: An upper bound for minimal resolution refutations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263797)