Research And Design Of Knowledge Reasoning Based On Machine Learning

Satisfaction is an important research task in the field of knowledge reasoning.In logic and computer science,the Boolean satisfiability problem(SAT)is the issue of finding if there exists an interpretation that makes a given Boolean formula satisfy.SAT is the first problem that was proven to be NP-complete.That is to say,there is no guarantee that the problem can be solved in polynomial time complexity.SAT is highly applied in the fields of artificial intelligence,circuit design,and automatic theorem proving.The complete,backtracking-based search algorithm Davis-Putnam-Logemann-Loveland(DPLL)algorithm can be used to solve SAT.However,as the scale of the problem and the difficulty increase,the complete algorithms may take a very long time.Although the incomplete algorithms proposed later have improved the problem solving speed to a certain extent,they also have obvious disadvantages,one being that they cannot prove the unsatisfiability of the problem.With the coming of the Machine Learning,many methods that apply neural networks to solve SAT have emerged.However,the use of neural network models to solve SAT can improve efficiency,the accuracy cannot be guaranteed when facing with difficult problems.In this case,the complete algorithms,incomplete algorithms and neural network models have their own merits and weaknesses.The simple use of one approach cannot guarantee the accuracy as well as efficiency.In view of the current situation,this paper proposes a solution to the SAT based on a combination of multiple models.Multiple models refer to multiple neural network models and a deterministic solver.Specifically,multiple neural network models include improved graph induction learning model,glue variables prediction based on reinforcement learning,and variables values prediction model based on Survey Propagation algorithm.Among them,we abstract the SAT problem as a graph model,and use an improved graph induction representation learning model to learn the relationships between nodes to adapt to different problem structures,and then use the reinforcement learning model to find the key variables of the problem,that is,glue variables.At the same time,the value prediction model is applied to predict the value of the variables.After the two are combined,the original problem can be simplified.Finally,the simplified problem is transferred to the deterministic solver to obtain its satisfiability.In terms of experiments,we selected part of the competition data sets from SATCompetition 2007-2020 to verify the performance of our model,and evaluated our solver from the perspective of accuracy and solution time.The experimental results indicate that our model works better on more difficult problems.On the same data set,the solution time can be about 20%-95%quicker than the deterministic solver,while at the same time around 72%more accurate than neural model.