The Unreasonable Effectiveness of Alternation-Based Satisfiability Algorithms

General SAT problems have associated 2SAT problems. These 2SAT problems provide support for techniques that augment existing SAT algorithms and enable new algorithms. Alternation covers yield more general termination criteria for SAT algorithms. The implication graph of the one related 2SAT problem supports decomposing SAT problems into independently solvable and deferable parts. An example demonstrates the effectiveness of the decomposition on one DIMACS benchmark problem. Another related 2SAT problem manifests constraints not recognized by other techniques. The theoretical and practical implications of these results are open.