From spin glasses to hard satisfiable formulas

Abstract. We introduce a highly structured family of hard satisfiable 3-SAT formulas corresponding to an ordered spin-glass model from statistical physics. This model has provably “glassy ” behavior; that is, it has many local optima with large energy barriers between them, so that local search algorithms get stuck and have difficulty finding the true ground state, i.e., the unique satisfying assignment. We test the hardness of our formulas with two complete Davis-Putnam solvers, Satz and zChaff, and two incomplete solvers, WalkSAT and the recently introduced Survey Propagation algorithm SP. We compare our formulas to random XOR-SAT formulas and to two other generators of hard satisfiable instances, the minimum disagreement parity formulas of Crawford et al., and Hirsch’s hgen2. For the complete solvers the running time of our formulas grows exponentially in √ n, and exceeds that of random XOR-SAT formulas for small problem sizes. More interestingly, our formulas appear to be harder for WalkSAT than any other known generator of satisfiable instances.