Locality and Hard SAT-Instances

In this note we construct a family of SAT-instance based on Eulerian graphs which are aimed at being hard for resolution based SAT-solvers. We discuss some experiments made with instances of this type and how a solver can try to avoid at least some of the pitfalls presented by these instances. Finally we look at how the density of subformulae can influence the hardness of SAT instances.