Marginal Probability Prediction For Boolean Formula Based On Graph Neural Networks

The marginal probability of Boolean formula is the probability that the target variable is assigned true among all assignments that make the Boolean propositional logic formula satisfiable.It is meaningful to calculate the marginal probabilities of Boolean formula.For example,if we can accurately randomly sample the variables in the formula,then the model counting can be derived from the marginal probabilities;if we can accurately calculate the marginal probabilities for all variables in the formula,then a satisfiable assignment of the formula can be generated quickly.Graph neural network refers to the combination of graph and neural network for end-to-end computing,which is convenient for processing structured data.Although the graph neural network method for solving the marginal probabilities for Boolean formulas has not been proposed,more and more researchers use graph neural networks to study problems related to Boolean logic formulas.Selsam et al.proposed an information transfer model based on graph neural network to solve the SAT problem.Abboud et al.proposed a method of using graph neural network to solve model count.This paper innovatively proposes a model named MargPred which applies graph neural network to solve the marginal probability of Boolean formula.The model expresses the CNF formulas as a graph,and establishes formula,clause and literal layer nodes respectively.The implicit dependencies of formulas,and the learning of the logical structure of formulas helps the network to learn how to solve problems.By setting the learning target of the network as a probability interval,rather than a specific probability,the problem is simplified,and the network can show useful performance.Not only that,this paper proposes a method to identify the target variable,which solves the problem of learning bias caused by only using formula embedding to calculate the probability distribution.By introducing the literal embedding of the specified variable,the model can learn the goal of solving the marginal distribution,and obtain better prediction results.MargPred incorporates a variety of popular neural network optimization methods,including gradient clipping,learning rate decay,l₂ regularization and Adam optimizer to prevent the model from overfitting during training.The paper also proposes a method ModelGen to generate a model of the Boolean formula,which uses MargPred to calculate the marginal probabilities of all the variables in the formula,picks the variable assignments with largest or smallest marginal probability and simplifies the formula,this process is repeated until the formula is completely reduced to get an assignment or current variable assignment has made the formula unsatisfiable.The algorithm of simplifying the formula adopts the Boolean constraint propagation algorithm,which follows the unit clause rules and can reduce the search space of formula variable assignment by nearly half.Finally get a set of assignments and verify that the assignment is a model of the formula.In order to verify the validity of the model MargPred,this paper compares MargPred with four models that adapt to the marginal distribution of the formula to solve this problem,and the prediction accuracy of MargPred is significantly better than other models.This paper also conducts ablation experiments on the robustness,the generalization ability of the problem scale,the classification of more probability intervals and the influence of the number of message transmissions,etc.,to verify the robustness of the model and explore how to make the model performance better.For the problem of generating a model for formulas,this paper compared the ModelGen method with another neural network method,and it turned out that ModelGen is far superior to other neural network methods,and even achieves 100%accuracy on simpler problems.