You can encode as moderately large (low hundreds of clauses/variables) SAT instances questions of Ramsey-theory and other unsolved combinatorics and those instances will not be solved by any heuristic.