The authors report on the results of an experimental study in which they have compared the performance of four algorithms for 2-SATISFIABILITY on 400 randomly generated test problems with up to 2000 variables and 8000 clauses (half of these problems were known a priori to be satisfiable). The four algorithms are: (1) the ‘serial’ Guess and Deduce algorithm by Deming; (2) the ‘parallel’ or ‘devetailing’ Guess and Deduce algorithm by Even, Itai, and Shamir; (3) the present Switching algorithm; (4) the Strong Components algorithm by Aspvall, Plass, and Tarjan. When the test problems are sampled from a uniform distribution, the authors have observed the following phenomenon: all the strong components of the implication graph are singletons, except for one (in the unsatisfiable case) or two (in the satisfiable case) ‘megacomponents’. In order to eliminate these and other related anomalies, they have built another instance generator which gives rise to strong components with binomially distributed sizes. An interesting outcome of the present experiments is that, under both probability models, the serial Guess and Deduce algorithm turns out to be the fastest one, in spite of its nonlinear worst-case complexity; whereas the Strong Components algorithm whose worst-case complexity is linear, turns out to be the slowest one.
