Locality and Hard SAT-Instances
Klas Markström · Journal on Satisfiability Boolean Modeling and Computation · 2006
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 o