基于消息传递关系网络的布尔可满足性预测

布尔可满足性求解能够验证的问题规模通常受限, 因此, 如何高精度地预测布尔可满足性问题的可满足性是一个重要研究问题, 也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构, 但是这种表征方法缺少了变量、子句之间的重要关系信息.在我们的方法中, 通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系, 并设计使用消息传递关系网络模型来捕获实例的关系信息, 提取了更多的结构特征.结果表明, 该模型在预测精度、泛化能力和资源需求等方面均优于现有模型, 对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练, 在大规模数据集上预测的平均预测精度达到了80.8%.同时, 该模型对随机生成的非均匀随机问题的预测精度达到99%, 这意味着它学习了预测可满足性的重要特征.此外, 模型预测所花费的时间随着问题规模的增大也只是呈线性增长. 总结而言, 本文基于关系消息传递网络提出了一个预测精度更高, 泛化能力更好的布尔可满足性预测方法.