scientific article; zbMATH DE number 1342212

MaRDI QIDQ4263797zbMATH OpenFDO

Authors Hans Kleine Büning

Publication date 22 September 1999

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
• scientific article; zbMATH DE number 1929954
• Narrow proofs may be maximally long
• scientific article; zbMATH DE number 1304340

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
• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• scientific article; zbMATH DE number 1929954 (Why is no real title available?)
• An upper bound for the circuit complexity of existentially quantified Boolean formulas

This page was built for publication:

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