Increasing the Robustness of SAT Solving with Machine Learning Techniques

Theses

• Suggested Thesis Topics
• Completed Theses
  • Algebra und Diskrete Strukturen
  • Automatentheorie
  • Computational Logic
  • Knowledge-aware Artificial Intelligence
  • Logische Programmierung und Argumentation
  • Verifikation und formale quantitative Analyse
  • Wissensbasierte Systeme
• Currently Ongoing Theses

Toggle side column

Increasing the Robustness of SAT Solving with Machine Learning Techniques

Master's thesis by Enrique Matos Alfonso

•   Supervisor Steffen Hölldobler, Norbert Manthey
•   Wissensverarbeitung
•   21 April 2014 – 10 September 2014
•   Download

Algorithm portfolios have become very popular in SAT competitions. The portfolio together with a good algorithm selection model can solve more instances than the best algorithm. For the algorithm selection task normally machine learning techniques are used based on features computed from the SAT instances. When the algorithm selection model is tested on instances that were part of the training dataset the results are very accurate but when novel instances are included in the testing dataset the performance decreases.

The primary purpose of this thesis was to study the performance on novel instances of the algorithm selection models based on machine learning techniques. A portfolio of different configurations of the Riss solver was built. New features were proposed and ten versions of features computation were tested. Furthermore, Six versions of machine learning models were proposed for the algorithm selection task. Four of them were based on binary classification models that predict when the configurations are “good” or “bad” for the given instance. The remaining two models used the k-nearest neighbor algorithm and a selection method based on the maximum value of a weighted contribution to predict the algorithm that was going to be used on the instance. The models were tested on novel instances and also on the complete benchmark.

The obtained results show that the proposed features can be computed efficiently, having 96% of non redundant information. Only the models that were not based on binary classification could outperform the best configuration when tested on novel instances. It was observed that the best prediction models performed better than the best configuration and better than the Lingeling solver, when tested on the complete benchmark.