How Many Conflicts Does It Need to Be Unsatisfiable?

DOI10.1007/978-3-540-79719-7_23MaRDI QIDQ3502712zbMATH OpenOpenAlexWikidataFDO

Authors D. Scheder, Philipp Zumstein

Publication date 27 May 2008

Published in Theory and Applications of Satisfiability Testing – SAT 2008 (Search for Journal in Brave)

Full work available at URL https://madoc.bib.uni-mannheim.de/41139/1/conflicts-postprint.pdf

zbMATH Keywords

conflict graphLovász Local Lemmasatisfiabilityunsatisfiable formulas

Mathematics Subject Classification ID

Classical propositional logic (03B05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Unsatisfiable CNF formulas contain many conflicts
• Unsatisfiable linear CNF formulas are large and complex
• Minimally unsatisfiable CNF formulas
• A threshold for unsatisfiability
• Trivial, tractable, hard. A not so sudden complexity jump in neighborhood restricted CNF formulas

Cites work

• A new algorithm approach to the general Lovász local lemma with applications to scheduling and satisfiability problems (extended abstract)
• A Note on Unsatisfiable k-CNF Formulas with Few Occurrences per Variable
• Branching rules for satisfiability
• scientific article; zbMATH DE number 1943962 (Why is no real title available?)
• Lopsided Lovász Local lemma and Latin transversals
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On subclasses of minimal unsatisfiable formulas
• One More Occurrence of Variables Makes Satisfiability Jump from Trivial to NP-Complete
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• The complexity of facets resolved
• The complexity of some subclasses of minimal unsatisfiable formulas.
• The probabilistic method. With an appendix on the life and work of Paul Erdős.
• The size Ramsey number
• Theory and Applications of Satisfiability Testing
• Using Lovász local lemma in the space of random injections

Cited in

(4)

• New width parameters for SAT and \#SAT
• Unsatisfiable CNF formulas contain many conflicts
• Disjoint DNF tautologies with conflict bound two
• Theory and Applications of Satisfiability Testing

This page was built for publication: How Many Conflicts Does It Need to Be Unsatisfiable?

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