Abstract | On input a random 3-CNF formula of clauses-to-variables ratio r3 applies repeatedly
the following simple heuristic: Set to True a literal that appears in the maximum number of clauses,
irrespective of their size and the number of occurrences of the negation of the literal (ties are broken
randomly; 1-clauses when they appear get priority). We prove that for r3 < 3.42 this heuristic
succeeds with probability asymptotically bounded away from zero. Previously, heuristics of increasing
sophistication were shown to succeed for r3 < 3.26. We improve up to r3 < 3.52 by further exploiting
the degree of the negation of the evaluated to True literal. |