An experimental evaluation of fast approximation algorithms for the maximum satisfiability problem

Abstract

We evaluate the performance of fast approximation algorithms for MAX SAT on the comprehensive benchmark sets from the SAT and MAX SAT contests. Our examination of a broad range of algorithmic techniques reveals that greedy algorithms offer particularly striking performance, delivering very good solutions at low computational cost. Interestingly, their relative ranking does not follow their worst case behavior. Johnson’s deterministic algorithm is constantly better than the randomized greedy algorithm of Poloczek et al. [31], but in turn is outperformed by the derandomization of the latter: this 2-pass algorithm satisfies more than 99% of the clauses for instances stemming from industrial applications. In general it performs considerably better than nonoblivious local search, Tabu Search,WalkSat, and several state-of-the-art complete and incomplete solvers, while being much faster. But the 2-pass algorithm does not achieve the excellent performance of Spears’ computationally intense simulated annealing. Therefore, we propose a new hybrid algorithm that combines the strengths of greedy algorithms and stochastic local search to provide outstanding solutions at high speed: in our experiments its performance is as good as simulated annealing, achieving an average loss with respect to the best known value of less that 0.5%, while its speed is comparable to the greedy algorithms.