OKlibrary  0.2.1.6
GreenTao_2-4-4.hpp File Reference

Investigations on greentao_2(4) More...

Go to the source code of this file.


Detailed Description

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 OKsolver-2002).
  • greentao_2(4) > 420 with 6683 nodes (OKsolver-2002).
  • greentao_2(4) > 430 with 22267 nodes (OKsolver-2002).
  • greentao_2(4) > 440 with 77791 nodes (OKsolver-2002).
  • greentao_2(4) > 450 with 349914 nodes (OKsolver-2002).
  • greentao_2(4) > 460 with 12777 nodes (OKsolver-2002).
  • greentao_2(4) > 470 with 59506 nodes (OKsolver-2002).
  • greentao_2(4) > 471 with 58889 nodes (OKsolver-2002).
  • greentao_2(4) > 472 with 370222 nodes (OKsolver-2002).
  • 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_2002-O3-DNDEBUG -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_2002-O3-DNDEBUG -M -D16 GreenTao_2_4_512.cnf
       
    finished the first branch (~ 32768 nodes at depth 16) after 9 days (cs-wsok) 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_2-reductions=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_1-autarkies=31556781 number_of_initial_unit-eliminations=0 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=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 OKsolver-2002, though n=500 seems also difficult.

Definition in file GreenTao_2-4-4.hpp.