图搜索的智能立方：比较研究
人工智能
2025-01-30 v1
摘要
通过立方与征服并行求解是扩大 SAT 求解器处理难题实例的关键方法。虽然立方与征服在纯 SAT 问题上已取得成功，尤其是毕达哥拉斯三元组猜想，但其应用于带有 propagators 的 SAT 求解器时面临独特挑战，因为这些 propagators 在搜索期间会动态学习约束。我们以 SAT Modulo Symmetries（SMS）作为主要测试案例研究此问题，其中一种对称性破坏 propagator 通过学习约束消除等构图，从而缩小搜索空间。通过超过 1 万小时的大量实验，我们系统评估了三组经典组合问题上不同的立方与征服变体。我们的 methodology 结合预运行阶段收集已学习约束、各种立方策略以及通过算法配置和 LLM 生成的设计建议进行参数调优。全面实证评估为基于 propagator 的 SAT 求解提供了有效立方策略的新见解，我们最佳方法通过改进立方和参数调优实现 2-3 倍加速，在更难的实例上额外获得 1.5-2 倍提升。
关键词
引用
@article{arxiv.2501.17201,
title = {Smart Cubing for Graph Search: A Comparative Study},
author = {Markus Kirchweger and Hai Xia and Tomáš Peitl and Stefan Szeider},
journal= {arXiv preprint arXiv:2501.17201},
year = {2025}
}