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

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 consistently better than the randomized greedy algorithm of Poloczek et al. [2017], but in turn is outperformed by the derandomization of the latter: this two-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 two-pass algorithm does not achieve the excellent performance of Spears’s 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 assignment of less that 0.5%, while its speed is comparable to the greedy algorithms. © 2017 ACM.