A backbone-search heuristic for efficient solving of hard 3-SAT formulae

Abstract

Of late, new insight into the study of random k-SAT formulae has been gained from the introduction of a concept inspired by models of physics, the `backbone ' of a SAT formula which corresponds to the variables having a fixed truth value in all assignments satisfying the maximum number of clauses.