Boosting SAT-solver Performance on FACT Instances with Automatic Parameter Tuning

University essay from KTH/Skolan för datavetenskap och kommunikation (CSC)

Author: Daniil Pintjuk; [2015]

Keywords: ;

Abstract:

Previous work by Asketorp [2014] has shown that integer factorization with the best SAT-solvers is orders of magnitude slower then with general number field sieve (GNFS). However only default configurations for the tested SAT-solvers ware considered in thous tests therefor this rapport attempts to explore what difference use of good configurations would have made. Our method involved using automatic parameter tunning with the algorithm iterated local search (ILS). ILS was used to tune the sat solver Minisat. And the tuned configuration was compared with the default by timing Minisat runs with respective configurations. The results show that performance gains are far from being big enough to suggest that the SAT-solvers tested by Asketorp [2014], would have come much closer to the performance of GNFS if tuned configurations were used. However the performance gains achieved in this report are impressive enough to advocate the use of automated parameter tuning of Sat-solvers for specific sets of instances.

  AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)