OKlibrary  0.2.1.6
OrthogonalSquares.hpp File Reference

On investigations regarding mutually orthogonal latin squares. More...

Go to the source code of this file.


Detailed Description

On investigations regarding mutually orthogonal latin squares.

Todo:
Experiments with the example from [Knuth, Vol. 4, Fascicle 0]
  • Given dk10_rls (see ComputerAlgebra/Satisfiability/Lisp/Generators/LatinSquares.mac), the task is to find the (unique) orthogonal latin square dk10_o_hrls.
  • And this using the direct translation into a (boolean) SAT problem.
  • Easy for the OKsolver-2002:
    LS_b : strong_ls(10)$
    LS_o : orthogonality_cond_ls(dk10_rls)$
    F : [LS_b[1], union(LS_b[2],LS_o,row_symmetrybreaking_ls(10))]$
    SF : standardise_fcs(F)$
    output_fcs_v(sconcat("The orthogonal latin square problem (weak form) with dimension ", p, " and matrix according to DK."),SF[1],"KOLS.cnf",SF[2]);
    > OKsolver_2002-O3-DNDEBUG KOLS.cnf
    s SATISFIABLE
    c sat_status=1 initial_maximal_clause_length=10 initial_number_of_variables=1000 initial_number_of_clauses=18310 initial_number_of_literal_occurrences=39010 running_time(s)=862.1 number_of_nodes=361731 number_of_single_nodes=94 number_of_quasi_single_nodes=0 number_of_2-reductions=3801745 number_of_pure_literals=0 number_of_autarkies=2 number_of_missed_single_nodes=1338 max_tree_depth=63 number_of_table_enlargements=0 reduced_maximal_clause_length=2 reduced_number_of_variables=280 reduced_number_of_clauses=7960 reduced_number_of_literal_occurrences=16690 number_of_1-autarkies=0 number_of_initial_unit-eliminations=280 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=10080 file_name=KOLS.cnf
    k
       
  • But hard for march_pl ("march_pl KOLS.cnf": Aborted after 12 hours (where memory usage reached 1GB): progress was made, but unclear how long it will take).
  • Even easier for OKsolver-2002 with the added dual conditions:
    LS_b : strong_ls(10)$
    LS_o : orthogonality_strongcond_ls(dk10_rls)$
    Fs : [LS_b[1], union(LS_b[2],LS_o,row_symmetrybreaking_ls(10))]$
    SFs : standardise_fcs(Fs)$
    output_fcs_v(sconcat("The orthogonal latin square problem (strong form) with dimension ", p, " and matrix according to DK."),SFs[1],"KOLSs.cnf",SFs[2]);
    > OKsolver_2002-O3-DNDEBUG KOLSs.cnf
    s SATISFIABLE
    c sat_status=1 initial_maximal_clause_length=10 initial_number_of_variables=1000 initial_number_of_clauses=18410 initial_number_of_literal_occurrences=40010 running_time(s)=515.4 number_of_nodes=223649 number_of_single_nodes=1 number_of_quasi_single_nodes=0 number_of_2-reductions=2280396 number_of_pure_literals=0 number_of_autarkies=4 number_of_missed_single_nodes=264 max_tree_depth=48 number_of_table_enlargements=0 reduced_maximal_clause_length=2 reduced_number_of_variables=280 reduced_number_of_clauses=7970 reduced_number_of_literal_occurrences=16970 number_of_1-autarkies=0 number_of_initial_unit-eliminations=280 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=10080 file_name=KOLSs.cnf
       
    (just 8 1/2 minutes)
  • But still (too) hard for march_pl: stopped after 14 hours (where some progress was apparently made, but unclear how much; this time only 150MB memory usage).
  • Apparently hard for local search algorithms: rnovelty+ seems best.
    > ubcsat-okl -alg rnovelty+ -runs 10000 -cutoff 1000000 -i KOLSs.cnf
    Clauses = 18410
    Variables = 1000
    TotalLiterals = 40010
    FlipsPerSecond = 490886
    BestStep_Mean = 407466.394800
    Steps_Mean = 1000000.000000
    Steps_Max = 1000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 10.967400
    BestSolution_Median = 12.000000
    BestSolution_Min = 4.000000
    BestSolution_Max = 16.000000
       
    Of course, one should eliminate the unit-clauses in the input.
  • But it doesn't get much better:
    uSFs : standardise_fcs(cs2fcs(ucp_cs_0(SFs[1][2])))$
    output_fcs_v(sconcat("The orthogonal latin square problem (strong form) with dimension ", p, " and matrix according to DK, UCP applied."),uSFs[1],"uKOLSs.cnf",uSFs[2]);
    > ubcsat -alg rnovelty+ -runs 10000 -cutoff 1000000 -i uKOLSs.cnf
    > summary(E)
     sat            min              omin     
     0:10000   Min.   : 4.000   Min.   :  3544
               1st Qu.: 8.000   1st Qu.:138374
               Median :10.000   Median :318611
               Mean   : 9.736   Mean   :381306
               3rd Qu.:10.000   3rd Qu.:597135
               Max.   :14.000   Max.   :999867
       
    Interessting:
    > table(E$min)
       4    6    8    9   10   11   12   14
      37  291 2305    1 5700    5 1647   14
       
  • Also with more steps it's hard to break through the barrier min=4:
    > ubcsat-okl -alg rnovelty+ -runs 1000 -cutoff 10000000 -i uKOLSs.cnf
    Clauses = 10440
    Variables = 720
    TotalLiterals = 23040
    FlipsPerSecond = 687051
    BestStep_Mean = 3393163.045000
    Steps_Mean = 10000000.000000
    Steps_Max = 10000000.000000
    PercentSuccess = 0.00
    BestSolution_Mean = 7.476000
    BestSolution_Median = 8.000000
    BestSolution_Min = 4.000000
    BestSolution_Max = 10.000000
       
  • Finally 1 success out of 100 with 10^8 steps:
    > ubcsat-okl -alg rnovelty+ -runs 100 -cutoff 100000000 -i uKOLSs.cnf
    Clauses = 10440
    Variables = 720
    TotalLiterals = 23040
    FlipsPerSecond = 721981
    BestStep_Mean = 32119641.610000
    Steps_Mean = 99329630.960000
    Steps_Max = 100000000.000000
    PercentSuccess = 1.00
    BestSolution_Mean = 5.560000
    BestSolution_Median = 6.000000
    BestSolution_Min = 0.000000
    BestSolution_Max = 8.000000
    > table(E$min)
     0  4  6  8
     1 26 66  7
       
    (seed = 3644605810).
  • Also unsatisfiability, when forbidding the single solution, is relatively easy for the OKsolver-2002:
    Fs_s : [LS_b[1], union(LS_b[2],LS_o,row_symmetrybreaking_ls(10),{exluding_solution_ls(dk10_o_hrls)})]$
    SFs_s : standardise_fcs(Fs_s)$
    output_fcs_v(sconcat("The orthogonal latin square problem (strong form) with dimension ", p, " and matrix according to DK, with excluded solution."),SFs_s[1],"KOLSs_s.cnf",SFs_s[2]);
    
    s UNSATISFIABLE
    c sat_status=0 initial_maximal_clause_length=100 initial_number_of_variables=1000 initial_number_of_clauses=18411 initial_number_of_literal_occurrences=40110 running_time(s)=-538.6 number_of_nodes=1490035 number_of_single_nodes=20 number_of_quasi_single_nodes=0 number_of_2-reductions=15902639 number_of_pure_literals=0 number_of_autarkies=17 number_of_missed_single_nodes=1794 max_tree_depth=68 number_of_table_enlargements=0 reduced_maximal_clause_length=10 reduced_number_of_variables=280 reduced_number_of_clauses=7970 reduced_number_of_literal_occurrences=16980 number_of_1-autarkies=0 number_of_initial_unit-eliminations=280 number_of_new_2-clauses=0 maximal_number_of_added_2-clauses=0 initial_number_of_2-clauses=10080 file_name=KOLSs_s.cnf
       
    (roughly one hour).
  • Minisat needed 5.3 hours to show unsatisfiability.
  • march_pl was stopped after 11 1/2 hours.

Definition in file OrthogonalSquares.hpp.