Unsatisfiable cnf formulas need many conflicts
D Scheder, P Zumstein - arXiv preprint arXiv:0806.1148, 2008 - arxiv.org
D Scheder, P Zumstein
arXiv preprint arXiv:0806.1148, 2008•arxiv.orgA 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. A CNF formula without any conflicts is
satisfiable. The Lovasz Local Lemma implies that a k-CNF formula is satisfiable if each
clause conflicts with at most 2^ k/e-1 clauses. It does not, however, give any good bound on
how many conflicts an unsatisfiable formula has globally. We show here that every
unsatisfiable k-CNF formula requires 2.69^ k conflicts and there exist unsatisfiable k-CNF …
positively in one clause and negatively in the other. A CNF formula without any conflicts is
satisfiable. The Lovasz Local Lemma implies that a k-CNF formula is satisfiable if each
clause conflicts with at most 2^ k/e-1 clauses. It does not, however, give any good bound on
how many conflicts an unsatisfiable formula has globally. We show here that every
unsatisfiable k-CNF formula requires 2.69^ k conflicts and there exist unsatisfiable k-CNF …
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. A CNF formula without any conflicts is satisfiable. The Lovasz Local Lemma implies that a k-CNF formula is satisfiable if each clause conflicts with at most 2^k/e-1 clauses. It does not, however, give any good bound on how many conflicts an unsatisfiable formula has globally. We show here that every unsatisfiable k-CNF formula requires 2.69^k conflicts and there exist unsatisfiable k-CNF formulas with 3.51^k conflicts.
arxiv.org