OKlibrary
0.2.1.6

Investigations on greentao_4(3) More...
Go to the source code of this file.
Investigations on greentao_4(3)
Generated by output_greentaod_stdname(4,3,n) or output_greentaod_sb_stdname(4,3,n) at Maximalevel, and by "GTdSat 4 3 n" at C++ level.
Standard nested translation generated by output_greentao_standnest_stdname([3,3,3,3],n) or output_greentao_standnest_strong_stdname([3,3,3,3],n).
Logarithmic translation generated by output_greentao_logarithmic_stdname([3,3,3,3],n).
gsat 36 gsat v simple 37.2 gwsat 31.1 gsattabu 21.7 hsat 36.1 hwsat 35.4 walksat 84.3 walksattabu 48.6 walksattabu v nonull 49.7 novelty 51 novelty+ 50.7 adaptnovelty+ 22.2 rnovelty 53.6 rnovelty+ 49.7 saps 41.6 rsaps 37.8 sapsnr 42.3 rots 21.2 irots 38.6 samd 20.9
samd 20.950000 FlipsPerSecond = 100301 gsattabu 21.1 FlipsPerSecond = 68634 rots 21.17 FlipsPerSecond = 77399 adaptnovelty+ 22.66 FlipsPerSecond = 473934
adaptnovelty+ 13.24 min = 8 FlipsPerSecond = 457666 samd 13.67 min = 10 FlipsPerSecond = 95157 gsattabu 13.75 min = 10 FlipsPerSecond = 94661 rots 18.34 min = 15 FlipsPerSecond = 79853
adaptnovelty+ 9.41 min = 7 samd 11.37 min = 7 gsattabu 11.35 min = 8 rots 17.97 min = 15
> ubcsatokl runs 10 cutoff 1000000 alg adaptnovelty+ i GreenTao_43_400m2pp.cnf Clauses = 30761 Variables = 1600 TotalLiterals = 135432 FlipsPerSecond = 256674 BestStep_Mean = 368355.300000 Steps_Mean = 1000000.000000 Steps_Max = 1000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 15.200000 BestSolution_Median = 14.500000 BestSolution_Min = 14.000000 BestSolution_Max = 18.000000 > ubcsatokl runs 10 cutoff 1000000 alg adaptnovelty+ i GreenTao_43_400.cnf Clauses = 32364 Variables = 1600 TotalLiterals = 95092 FlipsPerSecond = 542299 BestStep_Mean = 481813.900000 Steps_Mean = 1000000.000000 Steps_Max = 1000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 9.800000 BestSolution_Median = 10.000000 BestSolution_Min = 6.000000 BestSolution_Max = 11.000000 adaptnovelty+ 15.2 min = 14 samd 80.4 min = 74 gsattabu 80.5 min = 71 rots 76.0 min = 72 walksat 116.5 min = 110
> ubcsatokl runs 10 cutoff 1000000 alg adaptnovelty+ i GreenTao_sb_43_400.cnf Clauses = 32367 Variables = 1600 TotalLiterals = 95095 FlipsPerSecond = 477555 BestStep_Mean = 525055.500000 Steps_Mean = 1000000.000000 Steps_Max = 1000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 9.700000 BestSolution_Median = 10.000000 BestSolution_Min = 9.000000 BestSolution_Max = 11.000000 adaptnovelty+ 9.7 min = 9 samd 11.5 min = 9 gsattabu 11.1 min = 9 rots 17.8 min = 16
> ubcsatokl runs 10 cutoff 1000000 alg adaptnovelty+ i GreenTao_sb_43_400m2pp.cnf Clauses = 30488 Variables = 1600 TotalLiterals = 133986 FlipsPerSecond = 281532 BestStep_Mean = 463622.700000 Steps_Mean = 1000000.000000 Steps_Max = 1000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 15.300000 BestSolution_Median = 15.500000 BestSolution_Min = 12.000000 BestSolution_Max = 17.000000 adaptnovelty+ 15.3 min = 12 samd 83.9 min = 73 gsattabu min = rots 79.2 min = 64
> ubcsatokl alg adaptnovelty+ runs 100 cutoff 1000000 i GreenTao_43_357.cnf clauses = 26471 Variables = 1428 TotalLiterals = 77628 FlipsPerSecond = 659761 BestStep_Mean = 447147.770000 Steps_Mean = 1000000.000000 Steps_Max = 1000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 2.330000 BestSolution_Median = 2.000000 BestSolution_Min = 1.000000 BestSolution_Max = 4.000000
> ubcsatokl alg adaptnovelty+ runs 1000 cutoff 10000000 i GreenTao_43_357.cnf Clauses = 26471 Variables = 1428 TotalLiterals = 77628 FlipsPerSecond = 628361 BestStep_Mean = 3492205.863000 Steps_Mean = 9675267.971000 Steps_Max = 10000000.000000 PercentSuccess = 5.90 BestSolution_Mean = 1.236000 BestSolution_Median = 1.000000 BestSolution_Min = 0.000000 BestSolution_Max = 2.000000
> ubcsatokl alg adaptnovelty+ runs 1000 cutoff 10000000 i GreenTao_43_364.cnf Clauses = 27420 Variables = 1456 TotalLiterals = 80440 FlipsPerSecond = 602655 BestStep_Mean = 3488853.231000 Steps_Mean = 9993570.374000 Steps_Max = 10000000.000000 PercentSuccess = 0.10 BestSolution_Mean = 2.195000 BestSolution_Median = 2.000000 BestSolution_Min = 0.000000 BestSolution_Max = 4.000000
> ubcsatokl alg adaptnovelty+ runs 1000 cutoff 10000000 i GreenTao_43_365.cnf Clauses = 27543 Variables = 1460 TotalLiterals = 80804 FlipsPerSecond = 598431 BestStep_Mean = 3608383.766000 Steps_Mean = 9990625.610000 Steps_Max = 10000000.000000 PercentSuccess = 0.10 BestSolution_Mean = 2.248000 BestSolution_Median = 2.000000 BestSolution_Min = 0.000000 BestSolution_Max = 4.000000
> ubcsatokl alg adaptnovelty+ runs 1000 cutoff 10000000 i GreenTao_43_367.cnf Clauses = 27805 Variables = 1468 TotalLiterals = 81580 FlipsPerSecond = 597684 BestStep_Mean = 3695380.296000 Steps_Mean = 9999170.437000 Steps_Max = 10000000.000000 PercentSuccess = 0.10 BestSolution_Mean = 2.468000 BestSolution_Median = 2.000000 BestSolution_Min = 0.000000 BestSolution_Max = 4.000000
> ubcsatokl alg adaptnovelty+ runs 1000 cutoff 10000000 i GreenTao_43_368.cnf Clauses = 27936 Variables = 1472 TotalLiterals = 81968 FlipsPerSecond = 601632 BestStep_Mean = 3627492.165000 Steps_Mean = 9984052.649000 Steps_Max = 10000000.000000 PercentSuccess = 0.30 BestSolution_Mean = 2.580000 BestSolution_Median = 3.000000 BestSolution_Min = 0.000000 BestSolution_Max = 4.000000
> ubcsatokl alg adaptnovelty+ runs 1000 cutoff 10000000 i GreenTao_43_370.cnf Clauses = 28202 Variables = 1480 TotalLiterals = 82756 FlipsPerSecond = 612643 BestStep_Mean = 3801288.200000 Steps_Mean = 10000000.000000 Steps_Max = 10000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 2.821000 BestSolution_Median = 3.000000 BestSolution_Min = 1.000000 BestSolution_Max = 4.000000
With cutoff=20000000 in 1295 runs one solution was found (seed=406385002). </li> </ol> </li> <li> n=375: <ol> <li> \verbatim > ubcsatokl alg adaptnovelty+ runs 3000 cutoff 10000000 i GreenTao_43_375.cnf Clauses = 28901 Variables = 1500 TotalLiterals = 84828 FlipsPerSecond = 587133 BestStep_Mean = 3945694.062333 Steps_Mean = 10000000.000000 Steps_Max = 10000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 3.491667 BestSolution_Median = 4.000000 BestSolution_Min = 1.000000 BestSolution_Max = 5.000000 ubcsatokl alg adaptnovelty+ runs 1000 cutoff 20000000 i GreenTao_43_375.cnf Clauses = 28901 Variables = 1500 TotalLiterals = 84828 FlipsPerSecond = 577930 BestStep_Mean = 7458479.743000 Steps_Mean = 20000000.000000 Steps_Max = 20000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 3.156000 BestSolution_Median = 3.000000 BestSolution_Min = 1.000000 BestSolution_Max = 5.000000 > ubcsatokl alg adaptnovelty+ runs 1000 cutoff 100000000 i GreenTao_43_375.cnf Clauses = 28901 Variables = 1500 TotalLiterals = 84828 FlipsPerSecond = 601664 BestStep_Mean = 31289071.326000 Steps_Mean = 100000000.000000 Steps_Max = 100000000.000000 PercentSuccess = 0.00 BestSolution_Mean = 2.463000 BestSolution_Median = 2.000000 BestSolution_Min = 1.000000 BestSolution_Max = 4.000000
> E = read_ubcsat("GreenTao_43_377.OUT2") 1 2 3 84 776 40 900
1 2 22 46 68
0 1 2 1 34 79 114
1 2 3 25 281 21 327
> ubcsatokl alg adaptnovelty+ runs 100 cutoff 4000000000 i GreenTao_43_378.cnf sat min osteps msteps seed 1 0 1 3247511031 4000000000 969465860 2 0 2 26424461 4000000000 3292184256 3 0 2 41342213 4000000000 2086282835 4 0 1 2670401695 4000000000 3600327435
> E = read_ubcsat("GreenTao_43_379.cnf_OUT") 1 2 34 190 224 > E = read_ubcsat("GreenTao_43_379.cnf_OUT2") 1 2 7 45 52
> nohup ubcsatokl runs 1000 cutoff 4000000000 alg adaptnovelty+ i GreenTao_43_381.cnf  tee GreenTao_43_381.cnf_OUT & > E = read_ubcsat("GreenTao_43_381.cnf_OUT") 1 2 3 49 624 28 701 > summary(E$osteps) Min. 1st Qu. Median Mean 3rd Qu. Max. 3.368e+06 2.945e+08 7.322e+08 1.041e+09 1.482e+09 3.955e+09
E = run_ubcsat("GreenTao_L_43333_380.cnf", runs=200,cutoff=1000000)
> table(E$best[E$alg=="adaptnoveltyp"]) 2 3 4 5 6 7 8 9 1 4 14 54 65 46 15 1 > table(E$best[E$alg=="gwsat"]) 4 5 6 7 8 9 10 11 3 15 36 36 50 40 16 4 > table(E$best[E$alg=="rnoveltyp"]) 4 6 8 9 10 11 12 13 14 15 16 17 18 19 20 1 1 4 4 6 10 19 25 27 42 26 17 13 4 1
1 2 3 4 5 6 1 26 168 490 285 30 1000
1 2 3 4 5 6 2 20 143 281 53 1 500
1 2 3 4 5 4 47 229 219 4 503
1 2 3 4 13 82 314 91 500
1 2 3 4 5 20 157 431 355 37 1000
1 2 3 4 5 20 146 404 390 40 1000
1 2 3 4 12 44 54 2 112 0 1 2 3 4 1 25 97 131 4 258
0 1 2 3 4 2 35 164 222 9 432 > E[E$min==0,] sat min osteps msteps seed 56 1 0 62431299 62431299 3732998098 70 1 0 18376184 18376184 2048479337
1 2 3 4 48 238 434 64 784
0 1 2 3 4 5 4 76 430 750 155 1 1416
1 2 3 4 5 6 30 239 786 848 96 1 2000
1 2 3 4 36 277 661 252 1226
1 2 3 4 40 222 244 19 525 1 2 3 24 106 60 190
1 2 3 4 96 538 431 5 1070
1 2 3 135 338 86 559
Precosat236 for n=377
> OKsolver_2002O3DNDEBUG D30 M F GreenTao_43_377.cnf Name of file, monitoring depth and number of monitoring nodes: GreenTao_43_377.cnf, 30, 1073741824 level: nodes processed, average nodes, predicted total nodes, time for monitoring node, average time, predicted remaining time s UNKNOWN c sat_status=2 initial_maximal_clause_length=4 initial_number_of_variables=1508 initial_number_of_clauses=29195 initial_number_of_literal_occurrences=85700 running_time(s)=96556.5 number_of_nodes=5442104 number_of_single_nodes=29075 number_of_quasi_single_nodes=0 number_of_2reductions=77078983 number_of_pure_literals=0 number_of_autarkies=32 number_of_missed_single_nodes=55540 max_tree_depth=140 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=2218981570 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=2262 file_name=GreenTao_43_377.cnf
> OKsolver_2002m2pp D30 M F GreenTao_43_377.cnf s UNKNOWN c sat_status=2 initial_maximal_clause_length=9 initial_number_of_variables=1128 initial_number_of_clauses=27684 initial_number_of_literal_occurrences=121758 running_time(s)=251956.6 number_of_nodes=6807637 number_of_single_nodes=1004 number_of_quasi_single_nodes=0 number_of_2reductions=88887630 number_of_pure_literals=3 number_of_autarkies=10 number_of_missed_single_nodes=1529 max_tree_depth=179 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=84 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=1128 file_name=GreenTao_43_377.cnf_m2pp_582
> OKsolver_2002O3DNDEBUG D30 M F GreenTao_sb_43_377.cnf s UNKNOWN c sat_status=2 initial_maximal_clause_length=4 initial_number_of_variables=1508 initial_number_of_clauses=29198 initial_number_of_literal_occurrences=85703 running_time(s)=152404.7 number_of_nodes=10367390 number_of_single_nodes=81451 number_of_quasi_single_nodes=0 number_of_2reductions=148752374 number_of_pure_literals=0 number_of_autarkies=23 number_of_missed_single_nodes=165112 max_tree_depth=136 number_of_table_enlargements=0 reduced_maximal_clause_length=0 reduced_number_of_variables=4 reduced_number_of_clauses=274 reduced_number_of_literal_occurrences=899 number_of_1autarkies=4253877291 number_of_initial_uniteliminations=4 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=2344 file_name=GreenTao_sb_43_377.cnf
> OKsolver_2002m2pp M D30 F GreenTao_sb_43_377.cnf s UNKNOWN c sat_status=2 initial_maximal_clause_length=9 initial_number_of_variables=1125 initial_number_of_clauses=27417 initial_number_of_literal_occurrences=120344 running_time(s)=419516.6 number_of_nodes=10894679 number_of_single_nodes=4 number_of_quasi_single_nodes=0 number_of_2reductions=138939484 number_of_pure_literals=0 number_of_autarkies=20 number_of_missed_single_nodes=508 max_tree_depth=84 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=278 number_of_initial_uniteliminations=0 number_of_new_2clauses=0 maximal_number_of_added_2clauses=0 initial_number_of_2clauses=1213 file_name=GreenTao_sb_43_377.cnf_m2pp_16337
Definition in file GreenTao_43.hpp.