Home > Papers

 
 
A Elimination Mechanism of Glue Variables for Solving SAT Problems in Linguistics
ZHANG Ziwei,ZHANG Yang *
School of Computer Science, Beijing University of Posts and Telecommunications, Beijing 100876;School of Computer Science, Beijing University of Posts and Telecommunications, Beijing 100876
*Correspondence author
#Submitted by
Subject:
Funding: none
Opened online:23 February 2021
Accepted by: none
Citation: ZHANG Ziwei,ZHANG Yang.A Elimination Mechanism of Glue Variables for Solving SAT Problems in Linguistics[OL]. [23 February 2021] http://en.paper.edu.cn/en_releasepaper/content/4753646
 
 
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;
 
 
 

For this paper
  • ● PDF (0B)
  • ● Revision 0 　　
  • ● Print this paper
  • ● Recommend this paper to a friend
  • ● Add to my favorite list

    Saved Papers

    Please enter a name for this paper to be shown in your personalized Saved Papers list

Tags
Add yours

Related Papers

Statistics
PDF Downloaded 11
Bookmarked 0
Recommend 0
Comments Array
Submit your papers