Investigations on greentao_2(4)
Problems are generated by output_greentao2_stdname(4,n) at Maxima level, or by "GTdSat 2 4 n" at C++ level.
 Todo:
 greentao_2(4) = 512

greentao_2(4) > 400 (trivial for OKsolver2002).

greentao_2(4) > 420 with 6683 nodes (OKsolver2002).

greentao_2(4) > 430 with 22267 nodes (OKsolver2002).

greentao_2(4) > 440 with 77791 nodes (OKsolver2002).

greentao_2(4) > 450 with 349914 nodes (OKsolver2002).

greentao_2(4) > 460 with 12777 nodes (OKsolver2002).

greentao_2(4) > 470 with 59506 nodes (OKsolver2002).

greentao_2(4) > 471 with 58889 nodes (OKsolver2002).

greentao_2(4) > 472 with 370222 nodes (OKsolver2002).

For this n, rnovelty finds a solution quickly (~ 100000 steps).

n = 473: stopped after 884587 nodes (OKsolver).

But found satisfiable with rnovelty.

And rnovelty+ is even better.

n = 480: stopped after 1536394 nodes (OKsolver).

n = 500: Running it with
OKsolver_2002O3DNDEBUG M D18 F GreenTao_2_4_500.cnf
found a solution after 11 hours (38,937,288 nodes; roughly 2% of the search space, looking at depth 18).

Found satisfiable with rnovelty+.

n = 510 found satisfiable with rnovelty+.

n = 511 found satisfiable with rnovelty+.

n = 512: rnovelty+ yields constantly 1 falsified clause (also with "runs 500 cutoff 10000000").

OKplatform> OKsolver_2002O3DNDEBUG M D16 GreenTao_2_4_512.cnf
finished the first branch (~ 32768 nodes at depth 16) after 9 days (cswsok) and thus greentao_2(4) = 512.

Density is 8.7734375; here always counting all variables (though 2 variables are missing).

Stopped the computation:
33082: 7497, 780471.5, 765655.7
s UNKNOWN
c sat_status=2 initial_maximal_clause_length=4 initial_number_of_variables=510 initial_number_of_clauses=4492 initial_number_of_literal_occurrences=17968 running_time(s)=780475.6 number_of_nodes=765469925 number_of_single_nodes=58 number_of_quasi_single_nodes=0 number_of_2reductions=4696146230 number_of_pure_literals=728446 number_of_autarkies=2 number_of_missed_single_nodes=11248 max_tree_depth=61 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=0 reduced_number_of_clauses=0 reduced_number_of_literal_occurrences=0 number_of_1autarkies=31556781 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=0 file_name=GreenTao_2_4_512.cnf

n = 515: rnovelty+ yields constantly 1 falsified clause.

n = 520: rnovelty+ yields constantly 1 falsified clause.

n = 530: rnovelty+ yields constantly 1 falsified clause.

n = 540: rnovelty+ yields constantly 1 falsified clause.

n = 550: rnovelty+ yields constantly 2 falsified clauses.

n = 600: rnovelty+ yields constantly 6 falsified clauses.

Minisat looks weak on these instances.

And Grasp likely doesn't work here neither.

But march_pl seems stronger on the satisfiable instances than OKsolver2002, though n=500 seems also difficult.
Definition in file GreenTao_244.hpp.