Master Thesis Defense by Mr Enrique Matos
Mr Enrique Matos defended his master thesis on 'Increasing the Robustness of SAT Solving with Machine Learning Techniques'
Mr Enrique Matos defended his master thesis on 'Increasing the Robustness of SAT
Solving with Machine Learning Techniques' at TUD on 29 September 2014.
Abstract:
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.