Strong Refutation Heuristics for Random k-SAT

A simple first moment argument shows that in a randomly chosen k-SAT formula with m clauses over n boolean variables, the fraction of satisfiable clauses is 1−2−k +o(1) as m/n → ∞ almost surely. In this paper, we deal with the corresponding algorithmic strong refutation problem: given a random k-SAT formula, can we find a certificate that the fraction of satisfiable clauses is 1 − 2−k + o(1) in polynomial time? We present heuristics based on spectral techniques that in the case k = 3 and m ≥ ln(n)6 n3/2 , and in the case k = 4 and m ≥ Cn2 , find such certificates almost surely. In addition, we present heuristics for bounding the independence number (resp. the chromatic number) of random k-uniform hypergraphs from above (resp. from below) for k = 3, 4.

• Type: Conference
• Year: 2004
• Where: APPROX
• Authors: Amin Coja-Oghlan, Andreas Goerdt, André Lanka
• Keywords: Algorithms, APPROX 2004, K-SAT Formula, Satisfiable Clauses, first Moment Argument