学习优化合金分析仪

约束求解是场景查找工具的一个昂贵阶段。广泛观察到没有一个单一的“主导”SAT求解器在所有情况下总是胜出；相反，不同求解器的性能因情况而异。一些SAT求解器在某些任务上表现特别好，而其他求解器则在其他任务上表现良好。在本文中，我们提出了一种方法，利用机器学习技术根据从给定模型中提取的特征自动选择一种广泛使用的场景查找工具——合金分析仪的SAT求解器。目标是为给定模型选择最佳的SAT求解器，以最小化昂贵的约束求解时间。我们从三个不同的层次提取特征，即合金源代码层、Kodkod公式层和布尔公式层。实验结果表明，我们的组合方法比最佳SAT求解器的性能提高了30%，相比用户随机为任何给定模型选择求解器的基线方法提高了128%.