Exhaustive enumeration unveils clustering and freezing in random 3-SAT

TL;DR

This paper investigates the structure of solutions in random 3-SAT problems, revealing clustering and freezing phenomena that relate to computational hardness, and confirms theoretical predictions through empirical analysis.

Contribution

It provides the first detailed empirical analysis of solution clustering and freezing in random 3-SAT, validating theoretical asymptotic predictions for moderate system sizes.

Findings

Number of solution clusters matches theoretical predictions

Identified the freezing transition in the solution space

Frozen solutions are linked to computational hardness

Abstract

We study geometrical properties of the complete set of solutions of the random 3-satisfiability problem. We show that even for moderate system sizes the number of clusters corresponds surprisingly well with the theoretic asymptotic prediction. We locate the freezing transition in the space of solutions which has been conjectured to be relevant in explaining the onset of computational hardness in random constraint satisfaction problems.