以不可满足核预测引导高性能 SAT 求解器
神经与进化计算
2019-07-23 v7
摘要
NeuroSAT 神经网络架构近期被提出用于预测命题公式的性质。当训练其预测玩具问题的可满足性时，它被证明能自行找到解与不可满足核。然而，作者认为利用该架构改进当前最优水平“没有明显路径”。在本工作中，我们训练一个简化的 NeuroSAT 架构来直接预测真实问题的不可满足核。我们修改了多个高性能 SAT 求解器，使其周期性地用 NeuroSAT 对变量出现在不可满足核中可能性的预测来替换其变量活跃度分数。修改后的 MiniSat 在 SAT-COMP 2018 标准 5000 秒超时内比原版多求解 10% 的问题。修改后的 Glucose 比原版多求解 11%，而修改后的 Z3 多求解 6%。当训练针对特定问题分布专门化时，增益更大；在一个来自调度领域的困难问题基准上，修改后的 Glucose 在一小时超时内比原版多求解 20% 的问题。我们的结果证明 NeuroSAT 能为真实问题上的高性能 SAT 求解器提供有效引导。
引用
@article{arxiv.1903.04671,
title = {Guiding High-Performance SAT Solvers with Unsat-Core Predictions},
author = {Daniel Selsam and Nikolaj Bjørner},
journal= {arXiv preprint arXiv:1903.04671},
year = {2019}
}