Reactive search for MAX-SAT: diversification-bias properties with prohibitions and penalties

Many incomplete approaches for SAT and MAX-SAT have been proposed in the last years. The objective of this investigation is not so much horseracing (beating the competition on selected benchmarks) but understanding the qualitative differences between the various approaches by analyzing simplified versions thereof. In particular, we focus on reactive search schemes where task-dependent and local properties in the configuration space are used for the dynamic on-line tuning of local search parameters. We consider the choice between prohibition-based and penalty-based reactive approaches, and the choice between considering all variables or only the variables appearing in unsatisfied clauses. On simplified versions we consider the trade-off between diversification and bias after starting from a local minimizer, the so called D-B plots. We then consider long runs of the complete algorithms on selected MAX-SAT instances, by measuring both the number of iterations (flips) and the CPU times required by the single iterations with efficient data structures. The results confirm the effectiveness of reactive approaches, in particular when combined with non-oblivious objective functions. Furthermore a complex non-linear behavior of penalty-based schemes is observed.