The local lemma is tight for SAT

摘要: We construct unsatisfiable k-CNF formulas where every clause has k distinct literals and variable appears in at most (2/e +o(1)) 2k/k clauses. The lopsided Local Lemma shows that our result is asymptotically best possible: formula 2k+1/e(k+1) − 1 clauses satisfiable. determination of this extremal function particularly important as it represents the value k-SAT problem exhibits its complexity hardness jump: from having instance being a YES-instance becomes NP-hard just by allowing each to occur one more clause.The asymptotics other related functions are also determined. Let l(k) denote maximum number, such with containing common clauses, establish bound on obtained optimal, i.e., = (1/e + o(1)) 2k.The constructed all class MU(1) minimal than variables thus they resolve these asymptotic questions within well.The SAT-formulas via binary trees [10]. In order continuous setting defined, giving rise differential equation. solution equation diverges 0, which turn implies tree discretization required properties.