OKlibrary
0.2.1.6

Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,3,4]) More...
Go to the source code of this file.
Investigations regarding the "transversal extension" numbers greentao_{m+2}([2,...,2,3,4])
The aloamotranslation is generated by output_greentao_stdname(append(create_list(2,i,1,m),[3,4]),n) and output_greentao_sb_stdname(append(create_list(2,i,1,m),[3,4]),n) at Maximalevel, and by "GTSat 2 ... 2 3 4 n" at C++ level.
The nested translation is generated by output_greentao_standnest_stdname(append(create_list(2,i,1,m),[3,4]),n) and output_greentao_standnest_strong_stdname(append(create_list(2,i,1,m),[3,4]),n).
The logarithmic translation is generated by output_greentao_logarithmic_stdname(append(create_list(2,i,1,m),[3,4]),n).
The reduced translation is created by output_greentao_reduced_stdname(append(create_list(2,i,1,m),[3,4]),n) resp. output_greentao_reduced_strong_stdname(append(create_list(2,i,1,m),[3,4]),n).
> OKsolver_2002O3DNDEBUG GreenTao_3234_116.cnf s SATISFIABLE c sat_status 1 c initial_maximal_clause_length 4 c initial_number_of_variables 348 c initial_number_of_clauses 8061 c initial_number_of_literal_occurrences 17337 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 7018 c running_time(sec) 2.0 c number_of_nodes 2384 c number_of_single_nodes 0 c number_of_quasi_single_nodes 0 c number_of_2reductions 11743 c number_of_pure_literals 0 c number_of_autarkies 21 c number_of_missed_single_nodes 3 c max_tree_depth 76 c number_of_table_enlargements 0 c number_of_1autarkies 46284 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_3234_116.cnf > OKsolver_2002O3DNDEBUG GreenTao_3234_117.cnf s UNSATISFIABLE c sat_status 0 c initial_maximal_clause_length 4 c initial_number_of_variables 351 c initial_number_of_clauses 8198 c initial_number_of_literal_occurrences 17633 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 7137 c running_time(sec) 2.4 c number_of_nodes 2703 c number_of_single_nodes 0 c number_of_quasi_single_nodes 0 c number_of_2reductions 14339 c number_of_pure_literals 0 c number_of_autarkies 24 c number_of_missed_single_nodes 11 c max_tree_depth 77 c number_of_table_enlargements 0 c number_of_1autarkies 57409 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_3234_117.cnf
> OKsolver_2002O3DNDEBUG M D30 GreenTao_42234_130.cnf 227528557: 113 0.00 2.24E+04 0.80s 0.00s 0y 0d 0h 1m 15s 0 1 85 s UNKNOWN c sat_status 2 c initial_maximal_clause_length 4 c initial_number_of_variables 520 c initial_number_of_clauses 18821 c initial_number_of_literal_occurrences 39254 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 17550 c running_time(sec) 253.6 c number_of_nodes 44429 c number_of_single_nodes 37 c number_of_quasi_single_nodes 0 c number_of_2reductions 344658 c number_of_pure_literals 0 c number_of_autarkies 519 c number_of_missed_single_nodes 5154 c max_tree_depth 126 c number_of_table_enlargements 0 c number_of_1autarkies 5648488 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_42234_130.cnf
> E = run_ubcsat("GreenTao_522234_125.cnf")
> E = run_ubcsat("GreenTao_6222234_135.cnf")
> table(E$best[E$alg=="gwsat"]) 0 1 2 3 2 21 69 8 > table(E$best[E$alg=="rnovelty"]) 0 1 2 3 2 20 71 7 > table(E$best[E$alg=="sapsnr"]) 0 1 2 3 1 32 66 1 > table(E$best[E$alg=="rnoveltyp"]) 0 1 2 3 1 17 70 12 > table(E$best[E$alg=="saps"]) 1 2 49 51
n=136:
> OKsolver_2002O3DNDEBUG M D20 GreenTao_N_6222234_136.cnf 520192: 225216 3.88 4.07E+06 880.30s 0.01s 0y 0d 1h 58m 18s 119 0 213 s UNKNOWN c sat_status 2 c initial_maximal_clause_length 20 c initial_number_of_variables 679 c initial_number_of_clauses 37955 c initial_number_of_literal_occurrences 203255 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 9180 c running_time(sec) 17821.8 c number_of_nodes 4659973 c number_of_single_nodes 1568 c number_of_quasi_single_nodes 0 c number_of_2reductions 16952345 c number_of_pure_literals 155029 c number_of_autarkies 0 c number_of_missed_single_nodes 57156 c max_tree_depth 336 c number_of_table_enlargements 18 c number_of_1autarkies 6876472 c number_of_new_2clauses 0 c maximal_number_of_added_2clauses 0 c file_name GreenTao_N_6222234_136.cnf
0 1 2 9 78 13 100
0 1 2 37 62 1 100
1 2 77 23 100
1 2 99 1 100 > summary(E$osteps) Min. 1st Qu. Median Mean 3rd Qu. Max. 2209 70730 195600 919500 709400 9654000
> E = run_ubcsat("GreenTao_72222234_142.cnf", cutoff=1000000,runs=100) > plot(E$alg,E$best) > table(E$best[E$alg=="adaptnoveltyp"]) 1 100 > table(E$best[E$alg=="gwsat"]) 1 2 99 1 > table(E$best[E$alg=="noveltyp"]) 1 2 93 7 > table(E$best[E$alg=="saps"]) 1 2 78 22
> E = read_ubcsat("GreenTao_72222234_142.cnf_OUT3") 1 100 100 > summary(E$osteps) Min. 1st Qu. Median Mean 3rd Qu. Max. 43740 113900 205500 252300 346500 850900
1 2 39 61 100
1 2 3 4 8 52 38 2 100
1 2 44 56 100
1 2 526 474 1000
Definition in file GreenTao_te_m34.hpp.