How many conflicts does it need to be unsatisfiable?

Vorschau

PDF
conflicts-postprint.pdf - Angenommene Version
Download (143kB)

DOI:	https://doi.org/10.1007/978-3-540-79719-7_23
URL:	https://madoc.bib.uni-mannheim.de/41139
Weitere URL:	http://www2.cs.uni-paderborn.de/cs/ag-klbue/en/wor...
URN:	urn:nbn:de:bsz:180-madoc-411398
Dokumenttyp:	Konferenzveröffentlichung
Erscheinungsjahr:	2008
Buchtitel:	Theory and Applications of Satisfiability Testing - SAT 2008 : 11th International Conference, SAT 2008, Guangzhou, China, May 12 - 15, 2008; proceedings
Titel einer Zeitschrift oder einer Reihe:	Lecture Notes in Computer Science
Band/Volume:	4996
Seitenbereich:	246-256
Veranstaltungstitel:	SAT 2008 - 11th International Conference on Theory and Applications of Satisfiability Testing
Veranstaltungsort:	Guangzhou, China
Veranstaltungsdatum:	May 12 - 15, 2008
Herausgeber:	Kleine Büning, Hans
Ort der Veröffentlichung:	Berlin [u.a.]
Verlag:	Springer
ISBN:	978-3-540-79718-0 , 978-3-540-79719-7
ISSN:	0302-9743 , 1611-3349
Sprache der Veröffentlichung:	Englisch
Einrichtung:	Zentrale Einrichtungen > UB Universitätsbibliothek
Fachgebiet:	004 Informatik
Freie Schlagwörter (Englisch):	satisfiability , unsatisfiable formulas, conflict graph, Lovász Local Lemma
Abstract:	A pair of clauses in a CNF formula constitutes a conflict if there is a variable that occurs positively in one clause and negatively in the other. Clearly, a CNF formula has to have conflicts in order to be unsatisfiable—in fact, there have to be many conflicts, and it is the goal of this paper to quantify how many. An unsatisfiable k-CNF has at least 2^k clauses; a lower bound of 2^k for the number of conflicts follows easily. We improve on this trivial bound by showing that an unsatisfiable k-CNF formula requires Ω(2.32^k) conflicts. On the other hand there exist unsatisfiable k-CNF formulas with O((4^k(log k)^3)/k) conflicts. This improves the simple bound O(4^k) arising from the unsatisfiable k-CNF formula with the minimum number of clauses.
Zusätzliche Informationen:	The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-79719-7_23

	Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.
	Dieser Datensatz wurde nicht während einer Tätigkeit an der Universität Mannheim veröffentlicht, dies ist eine Externe Publikation.