论文标题
用胶水变量预测增强SAT求解器
Enhancing SAT solvers with glue variable predictions
论文作者
论文摘要
现代SAT求解器通常以尺度运行，这使得对每个分支决定的神经网络都不切实际。由Selsam和Bjorner提出的Neurocore提出了一种概念概念，即神经网络仍然可以通过定期重新调整基于得分的分支启发式来加速SAT求解器。但是，这项工作受到了几个限制：其修改后的求解器需要GPU加速，进一步的消融表明，它们不比SATCOMP 2018基准的随机基线更好，而他们的UNSAT核心培训目标需要昂贵的数据管道，这只有相对简单的不满意问题标记。我们使用更简单的网络体系结构来解决所有这些局限性，从而允许CPU推断数百万条子句的大量工业问题，并培训以预测{\ em胶水变量} ----一个目标，即更易于生成标记的数据，并且也可以将其作为强化学习任务表现出来。我们通过修改最先进的SAT求解器Cadical来证明我们的方法的有效性，从而在SATCOMP 2018和SATRACE 2019上的表现通过有监督的学习及其在SHA-1攻击数据集中的性能，并通过增强学习。
Modern SAT solvers routinely operate at scales that make it impractical to query a neural network for every branching decision. NeuroCore, proposed by Selsam and Bjorner, offered a proof-of-concept that neural networks can still accelerate SAT solvers by only periodically refocusing a score-based branching heuristic. However, that work suffered from several limitations: their modified solvers require GPU acceleration, further ablations showed that they were no better than a random baseline on the SATCOMP 2018 benchmark, and their training target of unsat cores required an expensive data pipeline which only labels relatively easy unsatisfiable problems. We address all these limitations, using a simpler network architecture allowing CPU inference for even large industrial problems with millions of clauses, and training instead to predict {\em glue variables}---a target for which it is easier to generate labelled data, and which can also be formulated as a reinforcement learning task. We demonstrate the effectiveness of our approach by modifying the state-of-the-art SAT solver CaDiCaL, improving its performance on SATCOMP 2018 and SATRACE 2019 with supervised learning and its performance on a dataset of SHA-1 preimage attacks with reinforcement learning.
