I'm trying to implement SAT solver, based on backtracking algorithm and BCP. This SAT solver is trying to pick one literal from each clause, from 3-CNF SAT instances. I've implemented a neural network based heuristic to pick valid literal at first, and degree of how valid is given literal from clause is determined by neural network output from 0.0 to 1.0 value. SAT instances on which I'm operating are big (hundreds of thousands clauses and similar amount of variables).
Currently I'm approaching about 97% accuracy on the training set, and about 90% accuracy on the test set, which means, that statistically, solver picks wrong literal in clause in 1 case out of 10, which is not bad, but not ideal.
The network has constant size vector at its input (about 30-40 neurons, depending on features that I'm picking in particular test scenario). The features are mainly some statistics about given SAT instance and situation which is currently solver in - they are derived from list of already solved literals, current clause, and clauses sharing literal, that I'm asking a netowrk to compute the score for. These features are commonly ratios, counts and conditionals (like 0.0 or 1.0 if given condition is present) - For example ratio of clauses reduced by choosing literal to the total clauses count, or ratio of trimmed clauses by this literal to total clauses count etc.
The score of 90% in the test set, is still not enough to solve such istances quicker. The question is, which features should i consider to add to the input ANN vector to achieve better accuracy?
Here is the list of used features in one of test scenarios: For the selected literal L in clause C (which is currently neural network focusing on), and partial solution S (which was previously selected literals - all valid):
- Number of clauses that has 3 literals, but under partial solution S, was reduced to 2 literal clauses
- Number of clauses that has 3 literals, but under partial solution S, was reduced to 1 literal clauses
- Number of clauses that has 2 literals, but under partial solution S, was reduced to 1 literal clauses
- Number of clauses that has N literals, but under partial solution S, has still N literals
- Number of clauses entirely removed under partial solution S (at least one literal in such clause belongs to S)
- Number of clauses sharing literal L
- Number of clauses sharing literal -L
- The same features as above, but repeated to one of other literal in clause C
By clauses sharing some literal L, I mean in these clauses L appears: for example 1,2,3 and 1,-4,5 (sharing literal is 1).
Above features are normalized, so the input vector is always valued between 0.0 and 1.0 for each feature.