A Elimination Mechanism of Glue Variables for Solving SAT Problems in Linguistics
首发时间:2021-02-23
Abstract:We propose GVE(Glue Variables Elimination), an algorithm that organically combines neural networks with a deterministic solver to solve SAT(Boolean satisfiability problem) in the filed of linguistics. It gives full play to their respective advantages by following steps: (a) finding the glue variables of the problem; (b) determining their values; (c) simplifying the original formula; (d) using a deterministic solver to solve the simplified problem. We use SATCOMP 2003-2019 benchmarks as the test data sets, and compare our model with the SAT solver CADICAL that has performed well in SATCOMP 2019 as well as the neural network models proposed in recent years. GVE model shows good performance. As the complexity of the problem increases, the solution time is much better than the deterministic solver, while at the same time more accurate than other neural network models.
keywords: computer technology boolean satisfaction problem graph learning survey propagation glue variables reinforcement learning
点击查看论文中文信息
求解布尔可满足性问题的胶合变量消除机制
摘要:我们针对布尔科满足性问题的求解提出了胶合变量消除模型(GVE),该模型将神经网络与确定性求解器进行了有机结合。他充分发挥了他们各自的优势,模型计算步骤如下:(1)找到布尔科满足性问题中的关键变量;(2)预测他们的值;(3)化简原始问题;(4)利用确定性求解器求解化简后的问题。我们使用了2003-2019年的布尔可满足性问题的求解大赛的比赛数据作为测试集,并且将我们的模型与在2019年的大赛中表现优异的求解器CADICAL和近年提出的神经网络模型作比较,GVE模型表现优异。随着问题的复杂度提升,所需求解时间少于确定性的求解器,同时比神经网络模型拥有更高的准确率。
基金:
引用
No.****
同行评议
勘误表
求解布尔可满足性问题的胶合变量消除机制
评论
全部评论0/1000