We'd like to use Graph Neural Networks, Graph Transformers to solve the SAT (more general Constraint Satisfaction Problem) and this repo is the PyTorch implementation of paper Transformers Satisfy and Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis
How to convert a CSP to k-SAT : For SAT, there are n binary variables and m constraints. Each constraint is associated with a k-tuple of (distinct) variables, for some k depending on the constraint, along with a subset of 
k which is the allowed assignments for the k-tuple of variables. For example, graph coloring, or rather, whether a given graph G can be x-colored, can be viewed as a CSP. If there are n vertices (we identify the vertex set with 
then we have n groups 
of 
variables. For each 
there is a constraint on each group 
stating that the assignment for is the binary encoding of a number in the range 
. For any two connected vertices )
there is a constraint on both groups 
stating that 
. This CSP is satisfiable iff G is x-colorable. In order to convert such a binary CSP to a SAT instance, we replace each constraint with the corresponding CNF. Continuing the example above, if 
then for any 
there is a constraint which we realize as  \wedge (\neg x_i \vee x_j))
. The resulting CNF is satisfiable iff the CSP is. You can use the standard reduction to convert this CNF to a 3CNF if you wish. We can also handle CSPs which are not binary, i.e., in which the variables are not binary but rather have some finite domain. The idea is similar to how I described coloring as a CSP above, and left to the reader.
(under the construction)
- Transformers are graph neural networks [link]
- PyTorch Geometric implementation of the Graph Attention Networks [link]
- Learning Local Search Heuristics for Boolean Satisfiability [paper, code]
- PDP Framework for Neural Constraint Satisfaction Solving [paper, code]