Generate a formula to begin
Random k-SAT formulas are generated by picking m = α·n clauses uniformly at random, each containing k randomly chosen variables (negated independently with probability 1/2). The resulting bipartite factor graph (variables × clauses) reveals the formula's structure. Hard instances near the threshold α_c ≈ 4.267 (for k=3) have dense, tangled factor graphs with many backbone variables — variables forced to a single value in all solutions.