HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation

Excerpt

arXiv:2409.18778v2 Announce Type: replace-cross Abstract: Efficiently determining the satisfiability of a boolean equation -- known as the SAT problem for brevity -- is crucial in various industrial problems. Recently, the advent of deep learning methods has introduced significant potential for enhancing SAT solving. However, a major barrier to the advancement of this field has been the scarcity of large, realistic datasets. The majority of current public datasets are either randomly generated o