A Sharp Hardness Transition in Tseitin Formulas Induced by Small Structural Perturbations

This dataset accompanies the SAT 2026 submission: "A Sharp Hardness Transition in Tseitin Formulas Induced by Small Structural Perturbations" We study hardness transitions in Tseitin formulas derived from Watts–Strogatz graphs.Small structural perturbations induce a sharp increase in CDCL solver runtime, strongly correlated with the spectral gap λ2. Solver instrumentation (Kissat 4.0.4) reveals that the transition is driven by a degradation in learned clause quality:- increasing approximate LBD- decreasing propagations per conflict- stable conflict rates The repository includes:- LaTeX source and PDF of the paper- publication-ready figures- experimental results (CSV)- scripts for analysis and plotting All experiments are deterministic and reproducible.