HardSATGEN：理解硬SAT公式生成的难度与一个强结构-硬度感知基线
HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline
AI总结：
HardSATGEN提出一种细粒度控制的神经拆分-合并方法，用于生成同时保持计算硬度和全局结构特性的工业SAT公式，显著优于现有方法。
摘要：
工业SAT公式生成是一项关键且具有挑战性的任务。现有的SAT生成方法难以同时捕捉全局结构特性并保持合理的计算硬度。我们首先对先前学习方法在再现原始实例计算硬度方面的局限性进行了深入分析，这种局限性可能源于它们所采用的拆分-合并过程中固有的同质性。基于工业公式表现出清晰的社区结构以及过度拆分的子结构导致逻辑结构语义形成困难的观察，我们提出了HardSATGEN，它在神经拆分-合并范式中引入了一种细粒度控制机制，用于SAT公式生成，以更好地恢复工业基准的结构和计算特性。包括在私有和实际企业测试平台上的评估在内的实验表明，HardSATGEN是唯一能够同时成功增强公式以保持相似计算硬度并捕捉全局结构特性的方法。与先前最佳方法相比，平均性能提升在结构统计上达到38.5%，在计算指标上达到88.4%，在我们生成的实例引导求解器调优的有效性上超过140.7%。源代码可在http://github.com/Thinklab-SJTU/HardSATGEN获取。
英文摘要：
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
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
