In this post, I will be taking a shot at building prediction models for learnt clause usefulness by running over 150 unsatisfiable CNF problems, extracting over 140 features for each learnt clause, and then calculating whether the clause was used in the UNSAT proof. Here I need to thank Marijn Heule who has helped me adding a clause ID to each clause in his DRAT checker so I could perform supervised learning on the collected data. Thanks Marijn!
The first works on machine learning in SAT has been by the crowd creating portifolio solvers such as SATZilla that calculate features of a CNF and then run the SAT solver that is predicted to solve that instance the fastest. This has been achieved by coming up with a set of easy-to-calculate but useful features and then using a standard prediction method to fit SAT solvers to CNFs. The issue, as always with machine learning, is overfitting. Unfortunately, CNFs tended to stay very similar between old SAT Competitions, and overfitting was richly rewarded. Hence, these portfolio solvers sometimes did well in competitions but sometimes relatively poorly in practice.
The second wave of improvements came with MapleSAT where a multi-armed bandit (MAB) framework was used to sometimes to pick branching variables. This won the 2016 SAT Competition‘s Main Track and was a novel and truly interesting idea, manipulating the branching heuristic based on the feature that the researchers called “learning rate“.
With this blog post, I hope to inspire a third wave of improvements in SAT solver performance. Learnt clause usefulness metrics have been a a very hot potato since the glucose SAT solver which engineered and used a new feature, glues, to decide the usefulness on. Maybe with the work and data provided below, we could use features not used before, or combine them in novel ways to achieve better prediction accuracy.