SAT problems with chains of dependent variables Original Research Article

This paper has two related themes. Firstly, artificial SAT problems are used to show that certain chains of variable dependency have a harmful effect on local search, sometimes causing exponential scaling on intrinsically easy problems. Secondly, systematic, local and hybrid SAT algorithms are evaluated on Hamiltonian cycle problems, exposing weaknesses in all three. The connection between the two themes is that some Hamiltonian cycle problems also cause local search to scale badly, indicating that pathological variable dependencies occur in more realistic applications. More generally, the results highlight the need for alternative models and search algorithms, and new examples of both are described.