Boosting Sequential Solver Portfolios: Knowledge Sharing and Accuracy Prediction

Abstract

Sequential algorithm portfolios for satisfiability testing (SAT), such as SATzilla and 3S, have enjoyed much success in the last decade. By leveraging the differing strengths of individual SAT solvers, portfolios employing older solvers have often fared as well or better than newly designed ones, in several categories of the annual SAT Competitions and Races. We propose two simple yet powerful techniques to further boost the performance of sequential portfolios, namely, a generic way of knowledge sharing suitable for sequential SAT solver schedules which is commonly employed in parallel SAT solvers, and a meta-level guardian classifier for judging whether to switch the main solver suggested by the portfolio with a recourse action solver. With these additions, we show that the performance of the sequential portfolio solver 3S, which dominated other sequential categories but was ranked 10th in the application category of the 2011 SAT Competition, can be boosted significantly, bringing it just one instance short of matching the performance of the winning application track solver, while still outperforming all other solvers submitted to the crafted and random categories.