Simple Algorithm Portfolio for SAT

TL;DR

This paper introduces a simple yet highly effective SAT solver portfolio that outperforms complex systems like SATzilla by selecting solvers based on the locality of similar instances.

Contribution

It presents a novel, straightforward algorithm portfolio for SAT that leverages local instance similarity for solver selection, achieving superior performance.

Findings

Outperforms SATzilla in efficiency and effectiveness

Uses k-nearest neighbors for solver selection

Simplifies the algorithm portfolio approach

Abstract

The importance of algorithm portfolio techniques for SAT has long been noted, and a number of very successful systems have been devised, including the most successful one --- SATzilla. However, all these systems are quite complex (to understand, reimplement, or modify). In this paper we propose a new algorithm portfolio for SAT that is extremely simple, but in the same time so efficient that it outperforms SATzilla. For a new SAT instance to be solved, our portfolio finds its k-nearest neighbors from the training set and invokes a solver that performs the best at those instances. The main distinguishing feature of our algorithm portfolio is the locality of the selection procedure --- the selection of a SAT solver is based only on few instances similar to the input one.