How many conflicts does it need to be unsatisfiable?


Scheder, Dominik ; Zumstein, Philipp


[img]
Preview
PDF
conflicts-postprint.pdf - Accepted

Download (143kB)

DOI: https://doi.org/10.1007/978-3-540-79719-7_23
URL: https://madoc.bib.uni-mannheim.de/41139
Additional URL: http://www2.cs.uni-paderborn.de/cs/ag-klbue/en/wor...
URN: urn:nbn:de:bsz:180-madoc-411398
Document Type: Conference or workshop publication
Year of publication: 2008
Book title: Theory and Applications of Satisfiability Testing - SAT 2008 : 11th International Conference, SAT 2008, Guangzhou, China, May 12 - 15, 2008; proceedings
The title of a journal, publication series: Lecture Notes in Computer Science
Volume: 4996
Page range: 246-256
Conference title: SAT 2008 - 11th International Conference on Theory and Applications of Satisfiability Testing
Location of the conference venue: Guangzhou, China
Date of the conference: May 12 - 15, 2008
Publisher: Kleine Büning, Hans
Place of publication: Berlin
Publishing house: Springer
ISBN: 978-3-540-79718-0 , 978-3-540-79719-7
Publication language: English
Institution: Zentrale Einrichtungen > University Library
Subject: 004 Computer science, internet
Keywords (English): 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.
Additional information: 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.




Metadata export


Citation


+ Search Authors in

BASE: Scheder, Dominik ; Zumstein, Philipp

Google Scholar: Scheder, Dominik ; Zumstein, Philipp

ORCID: Scheder, Dominik ; Zumstein, Philipp ORCID: 0000-0002-6485-9434

+ Download Statistics

Downloads per month over past year

View more statistics



You have found an error? Please let us know about your desired correction here: E-Mail


Actions (login required)

Show item Show item