It is not hard to find hard instances. Encode SHA256 in SAT, for one example. As for heuristics, etc, I strongly prefer approach that stems from observations v

It is not hard to find hard instances. Encode SHA256 in SAT, for one example. As for heuristics, etc, I strongly prefer approach that stems from observations valid for any problem. One such example is SDCL - Satisfaction Driven Clause Learning [1]. [1] https://publik.tuwien.ac.at/showentry.php?ID=266903&lang=6 https://publik.tuwien.ac.at/showentry.php?ID=266903&lang=6 They found a way to constrain search that needs selection - e.g., propagation has stopped and solver needs to select. This approach helps to solve pigeonhole problems much faster and is applicable outside of pigeonhole problems.