  Industrial SAT formula generation is a critical yet challenging task.
Existing SAT generation approaches can hardly simultaneously capture the global
structural properties and maintain plausible computational hardness. We first
present an in-depth analysis for the limitation of previous learning methods in
reproducing the computational hardness of original instances, which may stem
from the inherent homogeneity in their adopted split-merge procedure. On top of
the observations that industrial formulae exhibit clear community structure and
oversplit substructures lead to the difficulty in semantic formation of logical
structures, we propose HardSATGEN, which introduces a fine-grained control
mechanism to the neural split-merge paradigm for SAT formula generation to
better recover the structural and computational properties of the industrial
benchmarks. Experiments including evaluations on private and practical
corporate testbed show the superiority of HardSATGEN being the only method to
successfully augment formulae maintaining similar computational hardness and
capturing the global structural properties simultaneously. Compared to the best
previous methods, the average performance gains achieve 38.5% in structural
statistics, 88.4% in computational metrics, and over 140.7% in the
effectiveness of guiding solver tuning by our generated instances. Source code
is available at http://github.com/Thinklab-SJTU/HardSATGEN
