1
$\begingroup$

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?

EDIT:

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.

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ Perhaps it would be easier to come up with ideas for new features if we knew what features you're already using, so we don't duplicate them? The question doesn't list the features, you just say what they're derived from (also I don't know what "clauses sharing literal" means). It might be hard to make this kind of "brainstorming" / "come up with novel ideas for research" question work here on Stack Exchange. $\endgroup$
    – D.W. ♦
    Apr 3, 2021 at 22:18
  • $\begingroup$ Thank you for the comment. By sharing literals in some clauses, i mean literals that appears in every such clause, in other words, their common literals. I've listed features that i'm using in edit. $\endgroup$
    – komorra
    Apr 3, 2021 at 22:57
  • 1
    $\begingroup$ I don't think this question is a good fit here because there isn't going to be a single answer anyone can identify as correct. Using neural networks to attack Boolean satisfiability is an ongoing area of research, and at least one researcher isn't specifying problem features at all, he's letting a GNN find them. When SAT solvers augmented with deep learning start winning SAT solving competitions, then I think we will be able to answer this question. $\endgroup$
    – Kyle Jones
    Apr 4, 2021 at 2:41
  • 1
    $\begingroup$ Instead of adding an "EDIT:" section, please incorporate its contents to the body of the post. People reading your post in the future are not interested in its editing history. $\endgroup$
    – Yuval Filmus
    Apr 4, 2021 at 6:18
  • $\begingroup$ Are you using CDCL? Because it seems to me that giving your decision function more data by feeding conflict clauses back into the input is probably going to help more than most things, especially if you prioritise the newer information (somehow). $\endgroup$
    – Pseudonym
    Apr 7, 2021 at 0:57

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.