OKlibrary
0.2.1.6

Investigations on greentao_3(3) = 137. More...
Go to the source code of this file.
Investigations on greentao_3(3) = 137.
Aloamotranslation generated by output_greentaod_stdname(3,3,n) or output_greentaod_sb_stdname(3,3,n) at Maximalevel, and by "GTdSat 3 3 n" at C++ level.
Standard nested translation generated by output_greentao_standnest_stdname([3,3,3],n) or output_greentao_standnest_strong_stdname([3,3,3],n).
Logarithmic translation generated by output_greentao_logarithmic_stdname([3,3,3],n).
Standard reduced translation generated by output_greentao_reduced_stdname([3,3,3],n) or output_greentao_reduced_strong_stdname([3,3,3],n).
Clauses = 3614 Variables = 411 TotalLiterals = 10431 FlipsPerSecond = 1189726 BestStep_Mean = 162376.034000 Steps_Mean = 1000000.000000 Steps_Max = 1000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 1.000000 BestSolution_Median = 1.000000 BestSolution_Min = 1.000000 BestSolution_Max = 1.000000
> OKsolver_2002O3DNDEBUG D14 M F GreenTao_3333_137.cnf s UNSATISFIABLE c sat_status=0 initial_maximal_clause_length=3 initial_number_of_variables=411 initial_number_of_clauses=3614 initial_number_of_literal_occurrences=10431 running_time(s)=358228.8 number_of_nodes=517673976 number_of_single_nodes=8226277 number_of_quasi_single_nodes=0 number_of_2reductions=4048438213 number_of_pure_literals=0 number_of_autarkies=473887 number_of_missed_single_nodes=14846911 max_tree_depth=58 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=3256102327 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=411 file_name=GreenTao_3333_137.cnf
> NE = lm(E$time ~ E$nodes) > summary(NE) Residuals: Min 1Q Median 3Q Max 23.61630 0.02370 0.01408 0.02322 67.70912 Coefficients: Estimate Std. Error t value Pr(>t) (Intercept) 1.408e02 2.040e02 0.69 0.49 E$nodes 6.924e04 1.879e07 3685.43 <2e16 *** Residual standard error: 2.255 on 13850 degrees of freedom Multiple Rsquared: 0.999, Adjusted Rsquared: 0.999 Fstatistic: 1.358e+07 on 1 and 13850 DF, pvalue: < 2.2e16
> OKsolver_2002m2pp D10 M F GreenTao_3333_137.cnf s UNSATISFIABLE c sat_status=0 initial_maximal_clause_length=6 initial_number_of_variables=272 initial_number_of_clauses=3202 initial_number_of_literal_occurrences=12536 running_time(s)=6105.7 number_of_nodes=9573917 number_of_single_nodes=64902 number_of_quasi_single_nodes=0 number_of_2reductions=63127589 number_of_pure_literals=22228 number_of_autarkies=12674 number_of_missed_single_nodes=88075 max_tree_depth=52 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=227225 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=136 file_name=GreenTao_3333_137.cnf_m2pp_4279
> TN = lm(E$time ~ E$nodes) > summary(TN) Residuals: Min 1Q Median 3Q Max 9.8510128 0.0243738 0.0152368 0.0005773 8.8206325 Coefficients: Estimate Std. Error t value Pr(>t) (Intercept) 1.740e02 2.580e02 0.675 0.5 E$nodes 6.361e04 6.845e07 929.331 <2e16 *** Residual standard error: 0.7391 on 891 degrees of freedom Multiple Rsquared: 0.999, Adjusted Rsquared: 0.999 Fstatistic: 8.637e+05 on 1 and 891 DF, pvalue: < 2.2e16
> OKsolver_2002O3DNDEBUG M D10 F GreenTao_sb_33_137.cnf s UNSATISFIABLE c sat_status=0 initial_maximal_clause_length=3 initial_number_of_variables=411 initial_number_of_clauses=3616 initial_number_of_literal_occurrences=10433 running_time(s)=118149.6 number_of_nodes=169930659 number_of_single_nodes=2708740 number_of_quasi_single_nodes=0 number_of_2reductions=1325866058 number_of_pure_literals=0 number_of_autarkies=157007 number_of_missed_single_nodes=4893085 max_tree_depth=56 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=3 reduced_number_of_clauses=80 reduced_number_of_literal_occurrences=270 number_of_1autarkies=2150926704 number_of_initial_uniteliminations=3 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=445 file_name=GreenTao_sb_33_137.cnf
> TN = lm(E2$time ~ E2$nodes) > summary(TN) Residuals: Min 1Q Median 3Q Max 33.3498 0.7968 0.5493 0.1532 83.9398 Coefficients: Estimate Std. Error t value Pr(>t) (Intercept) 5.506e01 1.915e01 2.875 0.00413 ** E2$nodes 6.923e04 4.250e07 1628.727 < 2e16 *** Residual standard error: 5.359 on 933 degrees of freedom Multiple Rsquared: 0.9996, Adjusted Rsquared: 0.9996 Fstatistic: 2.653e+06 on 1 and 933 DF, pvalue: < 2.2e16
> SN = lm(E2$singles ~ E2$nodes) > summary(SN) Residuals: Min 1Q Median 3Q Max 3259.76 82.93 58.47 44.21 2392.32 Coefficients: Estimate Std. Error t value Pr(>t) (Intercept) 8.393e+01 1.722e+01 4.874 1.29e06 *** E2$nodes 1.548e02 3.822e05 405.008 < 2e16 *** Residual standard error: 481.8 on 933 degrees of freedom Multiple Rsquared: 0.9943, Adjusted Rsquared: 0.9943 Fstatistic: 1.64e+05 on 1 and 933 DF, pvalue: < 2.2e16
> AN = lm(E2$autarkies ~ E2$nodes) > summary(AN) Residuals: Min 1Q Median 3Q Max 816.997 14.188 4.524 4.293 2029.113 Coefficients: Estimate Std. Error t value Pr(>t) (Intercept) 4.293e+00 5.215e+00 0.823 0.411 E2$nodes 9.003e04 1.157e05 77.790 <2e16 *** Residual standard error: 145.9 on 933 degrees of freedom Multiple Rsquared: 0.8664, Adjusted Rsquared: 0.8663 Fstatistic: 6051 on 1 and 933 DF, pvalue: < 2.2e16
> OKsolver_2002m2pp D10 M F GreenTao_sb_33_137.cnf s UNSATISFIABLE c sat_status=0 initial_maximal_clause_length=6 initial_number_of_variables=270 initial_number_of_clauses=3127 initial_number_of_literal_occurrences=12164 running_time(s)=800.1 number_of_nodes=1240869 number_of_single_nodes=6668 number_of_quasi_single_nodes=0 number_of_2reductions=8108302 number_of_pure_literals=2701 number_of_autarkies=1427 number_of_missed_single_nodes=9847 max_tree_depth=55 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=8226 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=172 file_name=GreenTao_sb_33_137.cnf_m2pp_18152 \verbatim Average 2reductions ~ 6.5, and 270 / 6.5 ~ 41. Symmetry breaking is surprisingly effective here. </li> <li> The above "symmetry breaking" is "simple symmetry breaking", which should be the right form since we have k=3 here throughout. </li> <li> The above is the aloamotranslation; now with the (simple) logarithmic translation: \verbatim > OKsolver_2002O3DNDEBUG M D16 GreenTao_L_3333_137.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 274 c initial_number_of_clauses 3203 c initial_number_of_literal_occurrences 18670 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 137 c running_time(sec) 588.3 c number_of_nodes 997516 c number_of_single_nodes 341 c number_of_quasi_single_nodes 0 c number_of_2reductions 7829390 c number_of_pure_literals 210 c number_of_autarkies 291 c number_of_missed_single_nodes 1705 c max_tree_depth 48 c number_of_table_enlargements 0 c number_of_1autarkies 9672 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_L_3333_137.cnf
> OKsolver_2002O3DNDEBUG M D16 GreenTao_SR_3333_136.cnf s SATISFIABLE c sat_status 1 c initial_maximal_clause_length 6 c initial_number_of_variables 272 c initial_number_of_clauses 3163 c initial_number_of_literal_occurrences 12380 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 136 c running_time(sec) 93.9 c number_of_nodes 134508 c number_of_single_nodes 3762 c number_of_quasi_single_nodes 0 c number_of_2reductions 848045 c number_of_pure_literals 293 c number_of_autarkies 146 c number_of_missed_single_nodes 3467 c max_tree_depth 44 c number_of_table_enlargements 0 c number_of_1autarkies 1423 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_SR_3333_136.cnf > OKsolver_2002O3DNDEBUG M D16 GreenTao_SR_3333_137.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 274 c initial_number_of_clauses 3203 c initial_number_of_literal_occurrences 12538 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 137 c running_time(sec) 3994.1 c number_of_nodes 5576907 c number_of_single_nodes 150800 c number_of_quasi_single_nodes 0 c number_of_2reductions 35551956 c number_of_pure_literals 22901 c number_of_autarkies 12982 c number_of_missed_single_nodes 124384 c max_tree_depth 52 c number_of_table_enlargements 0 c number_of_1autarkies 144265 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_SR_3333_137.cnf
> OKsolver_2002O3DNDEBUG M D10 GreenTao_N_3333_137.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 272 c initial_number_of_clauses 3066 c initial_number_of_literal_occurrences 15330 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 0 c running_time(sec) 3234.0 c number_of_nodes 7068419 c number_of_single_nodes 22744 c number_of_quasi_single_nodes 0 c number_of_2reductions 30832450 c number_of_pure_literals 1931502 c number_of_autarkies 2933 c number_of_missed_single_nodes 26010 c max_tree_depth 65 c number_of_table_enlargements 0 c number_of_1autarkies 1527371 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_N_3333_137.cnf
> OKsolver_2002O3DNDEBUG M D10 GreenTao_SN_3333_137.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 274 c initial_number_of_clauses 3203 c initial_number_of_literal_occurrences 15604 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 137 c running_time(sec) 2588.2 c number_of_nodes 4368169 c number_of_single_nodes 15562 c number_of_quasi_single_nodes 0 c number_of_2reductions 26137544 c number_of_pure_literals 15036 c number_of_autarkies 12148 c number_of_missed_single_nodes 17394 c max_tree_depth 66 c number_of_table_enlargements 0 c number_of_1autarkies 748506 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_SN_3333_137.cnf
> system_directories/bin/OKsolver_2002_NTPO3DNDEBUG M D16 F GreenTao_33_137.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 3 c initial_number_of_variables 411 c initial_number_of_clauses 3614 c initial_number_of_literal_occurrences 10431 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 411 c running_time(sec) 726528.6 c number_of_nodes 1236624567 c number_of_single_nodes 0 c number_of_quasi_single_nodes 0 c number_of_2reductions 9821525375 c number_of_pure_literals 0 c number_of_autarkies 1019283 c number_of_missed_single_nodes 0 c max_tree_depth 58 c number_of_table_enlargements 0 c number_of_1autarkies 168173441743 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_33_137.cnf > E = read_oksolver_mon("GreenTao_33_137.cnf.mo") 62846 > plot_oksolver_mon_nodes(E) ldstep= 13 step= 8192 left= 128 right= 65536 obs/count= 1.042856 nodesrange= 1 1248779 avenodesrange= 5039.079 34624.96 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 1.0 19.0 804.5 19680.0 11700.0 1249000.0 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.500 7.440 7.900 8.003 8.170 44.000 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0 0 0 0 0 0 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.00 0.00 0.00 16.22 4.00 1514.00 Time ~ nodes: [1] 0.999718 (Intercept) E$nodes 0.0622892181 0.0005843438 Single nodes ~ nodes: [1] NaN (Intercept) E$nodes 0 0 Autarkies ~ nodes: [1] 0.723745 (Intercept) E$nodes 1.3708555637 0.0008939138 > hist_oksolver_mon_nodes(E) Median= 9.651948 Mean= 14.26423 > hist_oksolver_mon_nodes(E,breaks="st") Median= 9.651948
> system_directories/bin/OKsolver_2002_NTPO3DNDEBUG M D10 F GreenTao_sb_33_137m2pp.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 6 c initial_number_of_variables 270 c initial_number_of_clauses 3127 c initial_number_of_literal_occurrences 12164 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 172 c running_time(sec) 2855.8 c number_of_nodes 4972865 c number_of_single_nodes 0 c number_of_quasi_single_nodes 0 c number_of_2reductions 32618680 c number_of_pure_literals 7938 c number_of_autarkies 4427 c number_of_missed_single_nodes 0 c max_tree_depth 55 c number_of_table_enlargements 0 c number_of_1autarkies 30488 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_sb_33_137m2pp.cnf > E = read_oksolver_mon("GreenTao_sb_33_137m2pp.cnf.mo") 1024 > plot_oksolver_mon_nodes(E) ldstep= 7 step= 128 left= 128 right= 1024 obs/count= 1 nodesrange= 6 858348 avenodesrange= 2983.664 6898.701 > plot_oksolver_mon_nodes(E,ldstep=6) ldstep= 6 step= 64 left= 128 right= 1024 obs/count= 1 nodesrange= 6 858348 avenodesrange= 2983.664 6898.701 > summary_oksolver(E) Nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 6.0 145.0 354.5 4856.0 976.2 858300.0 2reductions: Min. 1st Qu. Median Mean 3rd Qu. Max. 1.830 6.328 6.540 6.542 6.750 8.530 Single nodes: Min. 1st Qu. Median Mean 3rd Qu. Max. 0 0 0 0 0 0 Autarkies: Min. 1st Qu. Median Mean 3rd Qu. Max. 0.000 0.000 0.000 4.323 0.000 361.000 Time ~ nodes: [1] 0.9998242 (Intercept) E$nodes 0.0052467076 0.0005731962 Single nodes ~ nodes: [1] NaN (Intercept) E$nodes 0 0 Autarkies ~ nodes: [1] 0.6404928 (Intercept) E$nodes 1.8800399269 0.0005030981 > hist_oksolver_mon_nodes(E,breaks="st") Median= 8.46964 Mean= 12.24565
c main():: nodeCount: 6473650 c main():: dead ends in main: 114820 c main():: lookAheadCount: 199038706 c main():: unitResolveCount: 51538014 c main():: time=874.280029 c main():: necessary_assignments: 150625 c main():: bin_sat: 0, bin_unsat 0 c main():: doublelook: #: 11816985, succes #: 9269815 c main():: doublelook: overall 6.191 of all possible doublelooks executed c main():: doublelook: succesrate: 78.445, average DL_trigger: 4303.527 s UNSATISFIABLE
Without symmetry breaking and without preprocessing:
> satz215m2pp GreenTao_3333_137.cnf NB_MONO= 1035059, NB_UNIT= 1785284987, NB_BRANCHE= 315959129, NB_BACK= 161499026 Program terminated in 5.792 seconds. satz215 GreenTao_3333_137.cnf_m2pp_18554 5.792 315959129 161499026 1880335698 722573320 0 411 3202 0 519236838 94536004
> satz215 GreenTao_sb_33_137.cnf NB_MONO= 0, NB_UNIT= 761352811, NB_BRANCHE= 23477136, NB_BACK= 12034648 Program terminated in 0.231 seconds. satz215 GreenTao_sb_33_137.cnf 0.231 23477136 12034648 745507284 61984415 0 411 3616 80 26757608 9227479
NB_MONO= 20243, NB_UNIT= 70999817, NB_BRANCHE= 3163421, NB_BACK= 1594481 Program terminated in 0.116 seconds. satz215 GreenTao_sb_33_137.cnf_m2pp_18306 0.116 3163421 1594481 404432467 18289941 0 411 3127 0 49387462 9601974
Definition in file GreenTao_33.hpp.