OKlibrary
0.2.1.6

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,3,3]) More...
Go to the source code of this file.
Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,3,3])
The aloamotranslation is generated by output_greentao_stdname(append(create_list(2,i,1,m),[3,3]),n) and output_greentao_sb_stdname(append(create_list(2,i,1,m),[3,3]),n) at Maximalevel, and by "GTSat 2 ... 2 3 3 n" at C++ level.
The nested translation is generated by output_greentao_standnest_stdname(append(create_list(2,i,1,m),[3,3]),n) and output_greentao_standnest_strong_stdname(append(create_list(2,i,1,m),[3,3]),n).
The logarithmic translation is generated by output_greentao_logarithmic_stdname(append(create_list(2,i,1,m),[3,3]),n).
The reduced translation is created by output_greentao_reduced_stdname(append(create_list(2,i,1,m),[3,3]),n) resp. output_greentao_reduced_strong_stdname(append(create_list(2,i,1,m),[3,3]),n).
> OKsolver_2002O3DNDEBUG M D10 F GreenTao_6222233_47.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 282 c initial_number_of_clauses 5372 c initial_number_of_literal_occurrences 11228 c number_of_initial_uniteliminations 0 c reddiff_maximal_clause_length 0 c reddiff_number_of_variables 0 c reddiff_number_of_clauses 0 c reddiff_number_of_literal_occurrences 0 c number_of_2clauses_after_reduction 5029 c running_time(sec) 2269.3 c number_of_nodes 4266000 c number_of_single_nodes 2217 c number_of_quasi_single_nodes 0 c number_of_2reductions 20413272 c number_of_pure_literals 0 c number_of_autarkies 63449 c number_of_missed_single_nodes 392532 c max_tree_depth 60 c number_of_table_enlargements 0 c number_of_1autarkies 236133359 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_6222233_47.cnf > E = read_oksolver_mon("GreenTao_6222233_47.cnf.mo") 1024 > plot_oksolver_mon_nodes(E,left=1) ldstep= 7 step= 128 left= 1 right= 1024 obs/count= 1 nodesrange= 5 75068 avenodesrange= 980.6 4937.533 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 5 614 1450 4166 4209 75070 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.500 3.710 4.270 4.663 5.115 33.600 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.000 0.000 0.000 2.165 1.000 120.000 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.00 3.00 12.00 61.96 40.00 1911.00 Time ~ nodes: [1] 0.9626347 (Intercept) E$nodes 0.0292801246 0.0005249267 Single nodes ~ nodes: [1] 0.03070471 (Intercept) E$nodes 1.3807603513 0.0001882563 Autarkies ~ nodes: [1] 0.7590312 (Intercept) E$nodes 14.99220801 0.01847188 > hist_oksolver_mon_nodes(E)
> OKsolver_2002m2pp M D10 F GreenTao_6222233_47.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 24 c initial_number_of_variables 229 c initial_number_of_clauses 4892 c initial_number_of_literal_occurrences 11898 c number_of_initial_uniteliminations 0 c reddiff_maximal_clause_length 0 c reddiff_number_of_variables 0 c reddiff_number_of_clauses 0 c reddiff_number_of_literal_occurrences 0 c number_of_2clauses_after_reduction 4596 c running_time(sec) 4716.8 c number_of_nodes 5175647 c number_of_single_nodes 216 c number_of_quasi_single_nodes 68 c number_of_2reductions 43341558 c number_of_pure_literals 137406 c number_of_autarkies 57622 c number_of_missed_single_nodes 133433 c max_tree_depth 121 c number_of_table_enlargements 0 c number_of_1autarkies 6498689 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_6222233_47.cnf_m2pp_6916 > E = read_oksolver_mon("GreenTao_6222233_47.cnf_m2pp_6916.mo") 1012 > plot_oksolver_mon_nodes(E,left=1) ldstep= 7 step= 128 left= 1 right= 1024 obs/count= 1.011858 nodesrange= 1 216013 avenodesrange= 2532.398 7640.75 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 1 51 382 5114 2094 216000 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.100 5.058 7.245 7.005 9.052 19.840 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.0000 0.0000 0.0000 0.2134 0.0000 25.0000 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.00 0.00 0.00 56.94 11.00 6168.00 Time ~ nodes: [1] 0.9898389 (Intercept) E$nodes 0.0882628069 0.0008940907 Single nodes ~ nodes: [1] 0.3890737 (Intercept) E$nodes 0.0560472614 0.0000526929 Autarkies ~ nodes: [1] 0.7921343 (Intercept) E$nodes 23.69363369 0.01576614 > hist_oksolver_mon_nodes(E)
> OKsolver_2002O3DNDEBUG M D10 F GreenTao_sb_6222233_47.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 282 c initial_number_of_clauses 5373 c initial_number_of_literal_occurrences 11230 c number_of_initial_uniteliminations 0 c reddiff_maximal_clause_length 0 c reddiff_number_of_variables 0 c reddiff_number_of_clauses 0 c reddiff_number_of_literal_occurrences 0 c number_of_2clauses_after_reduction 5030 c running_time(sec) 1105.8 c number_of_nodes 2101403 c number_of_single_nodes 948 c number_of_quasi_single_nodes 0 c number_of_2reductions 9937291 c number_of_pure_literals 0 c number_of_autarkies 31209 c number_of_missed_single_nodes 194102 c max_tree_depth 59 c number_of_table_enlargements 0 c number_of_1autarkies 115924859 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_sb_6222233_47.cnf > E = read_oksolver_mon("GreenTao_sb_6222233_47.cnf.mo") 1021 > plot_oksolver_mon_nodes(E,left=1) ldstep= 7 step= 128 left= 1 right= 1024 obs/count= 1.002938 nodesrange= 1 58477 avenodesrange= 49.333 2052.151 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 1 125 377 2058 1511 58480 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.200 3.260 4.050 4.358 5.220 34.670 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.0000 0.0000 0.0000 0.9285 0.0000 90.0000 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.00 0.00 3.00 30.57 12.00 1300.00 Time ~ nodes: [1] 0.9658678 (Intercept) E$nodes 0.0083875413 0.0005221542 Single nodes ~ nodes: [1] 0.04710342 (Intercept) E$nodes 0.4988707647 0.0002087429 Autarkies ~ nodes: [1] 0.7357201 (Intercept) E$nodes 5.82921479 0.01768372 > hist_oksolver_mon_nodes(E)
> OKsolver_2002m2pp M D10 F GreenTao_sb_6222233_47.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 16 c initial_number_of_variables 225 c initial_number_of_clauses 4730 c initial_number_of_literal_occurrences 11353 c number_of_initial_uniteliminations 0 c reddiff_maximal_clause_length 0 c reddiff_number_of_variables 0 c reddiff_number_of_clauses 0 c reddiff_number_of_literal_occurrences 0 c number_of_2clauses_after_reduction 4451 c running_time(sec) 216028.4 c number_of_nodes 215434556 c number_of_single_nodes 431683 c number_of_quasi_single_nodes 0 c number_of_2reductions 1878685678 c number_of_pure_literals 18025739 c number_of_autarkies 6866623 c number_of_missed_single_nodes 3724945 c max_tree_depth 82 c number_of_table_enlargements 0 c number_of_1autarkies 726406714 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_sb_6222233_47.cnf_m2pp_7718 > plot_oksolver_mon_nodes(E,left=1,ldstep=5) ldstep= 5 step= 32 left= 1 right= 1024 obs/count= 1.026052 nodesrange= 0 5536056 avenodesrange= 1.286 210385.3 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0 26 2169 215900 206800 5536000 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 1.22 8.51 9.29 11.46 13.48 66.00 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.0 0.0 5.0 432.5 389.5 9657.0 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.0 0.0 47.5 6880.0 6212.0 151500.0 Time ~ nodes: [1] 0.9951324 (Intercept) E$nodes 6.621237389 0.001033429 Single nodes ~ nodes: [1] 0.6542652 (Intercept) E$nodes 80.026281984 0.001633056 Autarkies ~ nodes: [1] 0.835877 (Intercept) E$nodes 434.35530177 0.02986121 > hist_oksolver_mon_nodes(E) Median= 11.08281 Mean= 17.71978
> OKsolver_2002O3DNDEBUG M D10 GreenTao_N_6222233_47.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 15 c initial_number_of_variables 234 c initial_number_of_clauses 4620 c initial_number_of_literal_occurrences 26060 c number_of_initial_uniteliminations 0 c reddiff_maximal_clause_length 0 c reddiff_number_of_variables 0 c reddiff_number_of_clauses 0 c reddiff_number_of_literal_occurrences 0 c number_of_2clauses_after_reduction 1081 c running_time(sec) 3142.2 c number_of_nodes 8578652 c number_of_single_nodes 7909 c number_of_quasi_single_nodes 0 c number_of_2reductions 17040065 c number_of_pure_literals 1574177 c number_of_autarkies 120 c number_of_missed_single_nodes 38374 c max_tree_depth 152 c number_of_table_enlargements 10 c number_of_1autarkies 417248 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_N_6222233_47.cnf
s UNSATISFIABLE c sat_status=0 initial_maximal_clause_length=7 initial_number_of_variables=371 initial_number_of_clauses=8415 initial_number_of_literal_occurrences=17453 running_time(s)=331416.7 number_of_nodes=176784736 number_of_single_nodes=1480233 number_of_quasi_single_nodes=0 number_of_2reductions=2961445595 number_of_pure_literals=0 number_of_autarkies=1108523 number_of_missed_single_nodes=3399131 max_tree_depth=63 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=15885525871 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=8004 file_name=GreenTao_sb_72222233_53.cnf
> OKsolver_2002m2pp M D15 F GreenTao_72222233_53.cnf GreenTao_72222233_53.cnf_m2pp_15229, 15, 32768 16255:4017096 14922.59 4.89E+08 4529.56s 17.95s 0y 3d 10h 21m 18s 1470 116746 153 s UNKNOWN c sat_status 2 c initial_maximal_clause_length 29 c initial_number_of_variables 310 c initial_number_of_clauses 7764 c initial_number_of_literal_occurrences 18809 c number_of_initial_uniteliminations 0 c reddiff_maximal_clause_length 0 c reddiff_number_of_variables 0 c reddiff_number_of_clauses 0 c reddiff_number_of_literal_occurrences 0 c number_of_2clauses_after_reduction 7400 c running_time(sec) 293581.0 c number_of_nodes 243777417 c number_of_single_nodes 78417 c number_of_quasi_single_nodes 840 c number_of_2reductions 2133168434 c number_of_pure_literals 14320249 c number_of_autarkies 5574285 c number_of_missed_single_nodes 14682434 c max_tree_depth 153 c number_of_table_enlargements 0 c number_of_1autarkies 464218661 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_72222233_53.cnf_m2pp_15229 > E = read_oksolver_mon("GreenTao_72222233_53.cnf_m2pp_15229.mo") 14724 > plot_oksolver_mon_nodes(E) ldstep= 11 step= 2048 left= 128 right= 16255 obs/count= 1.104355 nodesrange= 1 4626650 avenodesrange= 699.985 14922.59 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 1 13 102 16470 1265 4627000 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.100 5.750 8.860 8.824 11.200 90.000 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.000 0.000 0.000 5.312 0.000 2609.000 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.0 0.0 0.0 375.3 11.0 124100.0 Time ~ nodes: [1] 0.9886211 (Intercept) E$nodes 1.092014523 0.001136873 Single nodes ~ nodes: [1] 0.7498523 (Intercept) E$nodes 0.1662990797 0.0003325131 Autarkies ~ nodes: [1] 0.8931323 (Intercept) E$nodes 21.11046739 0.02406468 > hist_oksolver_mon_nodes(E) Median= 6.672425 Mean= 14.00792
 1474310763  463 11976 105386  170462 92053 150  1.678 %   2083501045  461 11861 104580  187509 43176 91  2.093 %   977767813  456 11576 102288  206260 42539 156  3.125 % 
> ubcsatokl alg adaptnovelty+ runs 100 cutoff 50000000 i GreenTao_12222222222233_71.cnf Clauses = 30221 Variables = 852 TotalLiterals = 61766 FlipsPerSecond = 347739 BestStep_Mean = 387364.340000 Steps_Mean = 50000000.000000 Steps_Max = 50000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 1.000000 BestSolution_Median = 1.000000 BestSolution_Min = 1.000000 BestSolution_Max = 1.000000
> E = run_ubcsat("GreenTao_L_12222222222233_70.cnf") > plot(E$alg,E$best) > eval_ubcsat_dataframe(E) gsat_tabu : 0 1 2 3 4 6 23 39 23 9 rsaps : 0 1 2 5 53 42 samd : 0 1 2 3 4 6 3 32 39 18 7 1 rots : 0 1 2 2 58 40 hwsat : 0 1 2 1 49 50 hsat : 0 1 2 3 4 1 8 59 26 6
with cutoff=10^6: gsattabu: 0 1 2 3 4 5 25 34 6 26 7 2 100 rsaps: 0 1 34 66 100 with cutoff=2*10^6: rsaps: 0 1 60 40 100
cutoff 10^5: 1 2 3 4 5 22 25 39 11 3 100 cutoff 10^6: 1 2 3 4 5 46 13 31 9 1 100
cutoff 10^5: 1 2 3 37 59 4 100 cutoff 10^6: 1 2 95 5 100
0 1 2 8 52 40 100
0 1 2 3 1 18 60 21 100
> E = run_ubcsat("GreenTao_L_132222222222233_73.cnf") > plot(E$alg,E$best) > eval_ubcsat_dataframe(E) rsaps : 1 2 42 58 gwsat : 1 2 3 25 72 3 rots : 1 2 3 24 74 2 walksat_tabu_nonull : 1 2 3 23 75 2 walksat_tabu : 1 2 22 78 irots : 1 2 22 78 hwsat : 1 2 3 4 14 59 25 2 sapsnr : 2 3 4 5 7 14 41 31 13 1 gsat_tabu : 1 2 3 4 5 6 7 8 10 39 33 8 1 1
> E = run_ubcsat("GreenTao_N_132222222222233_73.cnf") > plot(E$alg,E$best) > eval_ubcsat_dataframe(E) rsaps : 1 2 3 4 10 66 21 3 gsat_simple : 1 2 3 4 5 6 2 5 32 45 15 1 gwsat : 1 2 3 4 5 6 1 9 36 40 13 1 hsat : 1 2 3 4 5 6 1 7 31 42 18 1 gsat : 1 2 3 4 5 6 1 5 27 41 23 3
0 1 2 42 56 2 100
0 1 2 18 81 1 100
0 1 2 13 64 23 100
0 1 2 1 62 37 100
0 1 2 1 62 37 100
1 2 3 45 54 1 100
> E2=read_ubcsat("GreenTao_L_1422222222222233_79.cnf_OUT") 0 1 2 3 2 219 272 7 500 > E2[E2$min==0,] sat min osteps msteps seed 354 1 0 35553 35553 135591762 367 1 0 80973 80973 2195697436
1 2 3 4 8 258 220 14 500
1 2 3 4 24 344 131 1 500
1 2 3 53 411 36 500
1 2 3 89 410 1 500
1 2 307 693 1000
1 2 3 4 42 48 9 1 100
0 1 2 7 292 221 520
1 2 3 44 50 6 100 1 2 3 417 524 59 1000
> E = run_ubcsat("GreenTao_L_15222222222222233_83.cnf") > plot(E$alg,E$best) > eval_ubcsat_dataframe(E) walksat_tabu_nonull : 1 2 3 25 68 7 walksat_tabu : 1 2 3 23 69 8 rots : 1 2 3 19 56 25 irots : 1 2 3 4 17 60 22 1 rsaps : 1 2 3 4 15 56 25 4 hwsat : 1 2 3 4 5 10 30 36 21 3 gwsat : 1 2 3 5 60 35 rnoveltyp : 1 2 3 4 5 2 28 41 27 2 rnovelty : 1 2 3 4 5 2 19 48 25 6 novelty : 1 2 3 4 5 6 1 17 33 32 14 3 saps : 1 2 3 4 5 6 8 1 7 26 23 29 12 2 sapsnr : 1 2 3 4 5 6 7 1 1 16 39 27 12 4
1 2 3 2681 6903 416 10000
1 2 3 466 532 2 1000
1 2 3 4 20 39 40 1 100
0 1 2 3 4 10 63 24 2 1 100
0 1 2 17 64 19 100
1 2 3 4 5 31 50 14 100
1 2 3 4 3 47 45 5 100
1 2 3 4 14 57 27 2 100
1 2 3 4 25 66 8 1 100
> E = run_ubcsat("GreenTao_L_162222222222222233_86.cnf", runs=100,cutoff=1000000) > plot(E$alg,E$best) > eval_ubcsat_dataframe(E) hwsat : 1 2 77 23 gwsat : 1 2 72 28 rsaps : 1 2 72 28 irots : 1 2 72 28 walksat_tabu : 1 2 3 4 19 56 24 1
1 2 835 467 1302
Definition in file GreenTao_te_m33.hpp.