驱动 CDCL 搜索
人工智能
2016-11-17 v1
摘要
CDCL 算法是 SAT、SMT、ASP 等领域最先进的求解器所采用的主流方案。实验表明，通过嵌入领域特定的启发式策略，CDCL 求解器的性能可以得到显著提升，尤其是在大型现实世界问题上。然而，在现成的 CDCL 实现中恰当地集成此类准则并非易事。在本文中，我们提炼了驱动 CDCL 求解器搜索的关键要素，并提出了一个用于设计和实现新启发式策略的通用框架。我们在一个 ASP 求解器中实现了我们的策略，并在两个工业领域进行了实验。在困难的问题实例上，最先进的实现无法在可接受的时间内找到任何解，而我们的实现非常成功并找到了所有解。
引用
@article{arxiv.1611.05190,
title = {Driving CDCL Search},
author = {Carmine Dodaro and Philip Gasteiger and Nicola Leone and Benjamin Musitsch and Francesco Ricca and Konstantin Schekotihin},
journal= {arXiv preprint arXiv:1611.05190},
year = {2016}
}
备注
Paper presented at the 1st Workshop on Trends and Applications of Answer Set Programming (TAASP 2016), Klagenfurt, Austria, 26 September 2016, 15 pages, LaTeX, 5 figures