HardSATGEN：理解难 SAT 公式生成的困难性与一个强大的结构-难度感知基线
人工智能
2024-02-09 v3 机器学习
摘要
工业 SAT 公式生成是一项关键但具有挑战性的任务。现有的 SAT 生成方法很难同时捕捉全局结构特性并保持合理的计算难度。我们首先深入分析了先前学习方法在再现原始实例计算难度方面的局限性，这可能源于它们所采用的拆分-合并过程中固有的同质性。基于工业公式展现出清晰的社区结构，以及过度拆分的子结构导致逻辑结构语义形成困难的观察，我们提出了 HardSATGEN，它为 SAT 公式生成的神经拆分-合并范式引入了一种细粒度的控制机制，以更好地恢复工业基准的结构和计算特性。包括在私有和实际企业测试集上的评估在内的实验表明，HardSATGEN 是唯一能够成功增强公式，同时保持相似计算难度并捕捉全局结构特性的方法。与之前的最佳方法相比，其在结构统计量上的平均性能提升达到 38.5%，在计算指标上达到 88.4%，在通过我们生成的实例指导求解器调优的有效性上超过 140.7%。源代码可在 http://github.com/Thinklab-SJTU/HardSATGEN 获取。
引用
@article{arxiv.2302.02104,
title = {HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline},
author = {Yang Li and Xinyan Chen and Wenxuan Guo and Xijun Li and Wanqian Luo and Junhua Huang and Hui-Ling Zhen and Mingxuan Yuan and Junchi Yan},
journal= {arXiv preprint arXiv:2302.02104},
year = {2024}
}
备注
Published at SIGKDD 2023, see http://dl.acm.org/doi/10.1145/3580305.3599837