OKlibrary  0.2.1.6
Ramsey_2_5_5.hpp File Reference

On investigations into Ramsey problems of the form ramsey_2^2(5,5) More...

Go to the source code of this file.


Detailed Description

On investigations into Ramsey problems of the form ramsey_2^2(5,5)

Todo:
General information
  • Known is 43 <= ramsey_2^2(5) <= 49.
  • So we get 1-2 million clauses.
  • To generate an instance of SAT problem specifying "ramsey_2^2(5) > n?" use the following:
    Ramsey-O3-DNDEBUG 5 5 2 6 | ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_6.cnf
       
    where n has been replaced by 6 in this example.
  • To generate the additional clauses for each of the symmetry breaking techniques (see ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/plans/RamseyProblems.hpp) and cardinality constraints, run the following in maxima (generating each of the additional clauses for a range of n values):
    • Symmetry breaking by fixing colours/labels to break monochromatic k-subsets:
      for n : 5 thru 49 do output_ramsey2_symbr1_stdname(5,n);
          
    • Symmetry breaking by fixing monochromatic cliques:
      for n : 5 thru 49 do output_ramsey2_symbr2_stdname(n);
          
    • Symmetry breaking by recursive application of the pigeon hole principle:
      for n : 5 thru 49 do output_ramsey2_symbr3_stdname(n);
          
    • Cardinality constraints:
      :lisp (ext:set-limit 'ext:heap-size 3000000000)
      :lisp (ext:set-limit 'ext:frame-stack 10000)
      :lisp (ext:set-limit 'ext:c-stack 200000)
      :lisp (ext:set-limit 'ext:lisp-stack 200000)
      for n : 5 thru 49 do block([n_e : binomial(n,2)],
        output_fcs(
          sconcat("Card ",n),
          fcl2fcs(standardise_fcl(cl2fcl(unary_bb_crd2fcl([floor(n_e/2),create_list(i,i,1,n_e),ceiling(n_e/2)])))[1]),
          sconcat("Card_n",n,".cnf")))$
          
Todo:
Using DPLL and Conflict driven solvers
  • Initial investigations:
    • OKsolver can handle n=33 in ~ 3 minutes, but has problems with n=34.
    • march_pl seems to have problems already for n=30.
    • minisat can handle n=30 in 2 seconds; n=35 ?
    • UnitMarch: n=30 in 3 seconds, but n=33 unsolved after 20 minutes.
  • A more systematic investigation, involving each of the symmetry breaking techniques and cardinality constraints (see Experimentation/Investigations/RamseyTheory/RamseyProblems/plans/SymmetryBreaking.hpp) can be generated and run using the experiment system discussed at "General experiment system" in Experimentation/Investigations/Cryptography/AES/plans/BreakingAES.hpp), with the following "generate_exp.sh" script:
    # Generates Ramsey experiments for "ramsey_2^2(5,5) > n?" for 5 <= n <= 49.
    
    
    for n in `seq 5 49`; do
    # No Symmetry breaking
        echo "PICOSAT_"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./solvers/picosat913 -v Ramsey_exp.cnf > Ramsey_5_5_2_${n}.cnf.result.picosat 2>&1 && rm Ramsey_5_5_2_${n}.cnf" >> experiments;
        echo "MINISAT2_"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./solvers/minisat2 Ramsey_5_5_2_${n}.cnf minisat-temp > Ramsey_5_5_2_${n}.cnf.result.minisat2 2>&1; cat minisat-temp >> Ramsey_5_5_2_${n}.cnf.result.minisat2;rm Ramsey_5_5_2_${n}.cnf" >> experiments;
        echo "MARCH_PL_"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./solvers/march_pl Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}.cnf.result.march_pl 2>&1;rm Ramsey_5_5_2_${n}.cnf" >> experiments;
        echo "OKSOLVER_"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./solvers/OKsolver_2002-O3-DNDEBUG -O -D20 -M -F Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}.cnf.result.OKsolver 2>&1; mv Ramsey_5_5_2_${n}.cnf.mo Ramsey_5_5_2_${n}.cnf.mo.OKsolver;mv Ramsey_5_5_2_${n}.cnf.pa Ramsey_5_5_2_${n}.cnf.pa.OKsolver;rm Ramsey_5_5_2_${n}.cnf" >> experiments;
        echo "OKSOLVERM2PP_"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./solvers/OKsolver_2002-m2pp -O -D20 -M -F Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}.cnf.result.OKsolver-m2pp 2>&1; mv Ramsey_5_5_2_${n}.cnf_m2pp_*.mo Ramsey_5_5_2_${n}.cnf.mo.OKsolver-m2pp;mv Ramsey_5_5_2_${n}.cnf_m2pp_*.pa Ramsey_5_5_2_${n}.cnf.pa.OKsolver-m2pp;rm Ramsey_5_5_2_${n}.cnf" >> experiments;
    # Symmetry breaking 1
       echo "PICOSAT_FC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_FC_5_${n}.ecnf > Ramsey_5_5_2_${n}_SB_FC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_FC.ecnf > Ramsey_5_5_2_${n}_SB_FC.cnf && ./solvers/picosat913 -v Ramsey_exp.cnf > Ramsey_5_5_2_${n}_SB_FC.cnf.result.picosat 2>&1 && rm -f Ramsey_5_5_2_${n}{,_SB_FC}.{e,}cnf" >> experiments;
        echo "MINISAT2_FC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_FC_5_${n}.ecnf > Ramsey_5_5_2_${n}_SB_FC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_FC.ecnf > Ramsey_5_5_2_${n}_SB_FC.cnf && ./solvers/minisat2 Ramsey_5_5_2_${n}_SB_FC.cnf minisat-temp > Ramsey_5_5_2_${n}_SB_FC.cnf.result.minisat2 2>&1; cat minisat-temp >> Ramsey_5_5_2_${n}_SB_FC.cnf.result.minisat2;rm -f Ramsey_5_5_2_${n}{,_SB_FC}.{e,}cnf" >> experiments;
      echo "MARCH_PL_FC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_FC_5_${n}.ecnf > Ramsey_5_5_2_${n}_SB_FC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_FC.ecnf > Ramsey_5_5_2_${n}_SB_FC.cnf && ./solvers/march_pl Ramsey_5_5_2_${n}_SB_FC.cnf > Ramsey_5_5_2_${n}_SB_FC.cnf.result.march_pl 2>&1;rm -f Ramsey_5_5_2_${n}{_SB_FC,}.{e,}cnf" >> experiments;
       echo "OKSOLVER_FC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_FC_5_${n}.ecnf > Ramsey_5_5_2_${n}_SB_FC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_FC.ecnf > Ramsey_5_5_2_${n}_SB_FC.cnf && ./solvers/OKsolver_2002-O3-DNDEBUG -O -D20 -M -F Ramsey_5_5_2_${n}_SB_FC.cnf > Ramsey_5_5_2_${n}_SB_FC.cnf.result.OKsolver 2>&1; mv Ramsey_5_5_2_${n}_SB_FC.cnf.mo Ramsey_5_5_2_${n}_SB_FC.cnf.mo.OKsolver;mv Ramsey_5_5_2_${n}_SB_FC.cnf.pa Ramsey_5_5_2_${n}_SB_FC.cnf.pa.OKsolver;rm -f Ramsey_5_5_2_${n}{,_SB_FC}.{e,}cnf" >> experiments;
        echo "OKSOLVERM2PP_FC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_FC_5_${n}.ecnf > Ramsey_5_5_2_${n}_SB_FC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_FC.ecnf > Ramsey_5_5_2_${n}_SB_FC.cnf && ./solvers/OKsolver_2002-m2pp -O -D20 -M -F Ramsey_5_5_2_${n}_SB_FC.cnf > Ramsey_5_5_2_${n}_SB_FC.cnf.result.OKsolver-m2pp 2>&1; mv Ramsey_5_5_2_${n}_SB_FC.cnf_m2pp_*.mo Ramsey_5_5_2_${n}_SB_FC.cnf.mo.OKsolver-m2pp;mv Ramsey_5_5_2_${n}_SB_FC.cnf_m2pp_*.pa Ramsey_5_5_2_${n}_SB_FC.cnf.pa.OKsolver-m2pp;rm -f Ramsey_5_5_2_${n}{,_SB_FC}.{e,}cnf" >> experiments;
    # Symmetry breaking 2
       echo "PICOSAT_MC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_MC_${n}.ecnf > Ramsey_5_5_2_${n}_SB_MC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_MC.ecnf > Ramsey_5_5_2_${n}_SB_MC.cnf && ./solvers/picosat913 -v Ramsey_5_5_2_${n}_SB_MC.cnf > Ramsey_5_5_2_${n}_SB_MC.cnf.result.picosat 2>&1 && rm -f Ramsey_5_5_2_${n}{,_SB_MC}.{e,}cnf" >> experiments;
        echo "MINISAT2_MC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_MC_${n}.ecnf > Ramsey_5_5_2_${n}_SB_MC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_MC.ecnf > Ramsey_5_5_2_${n}_SB_MC.cnf && ./solvers/minisat2 Ramsey_5_5_2_${n}_SB_MC.cnf minisat-temp > Ramsey_5_5_2_${n}_SB_MC.cnf.result.minisat2 2>&1; cat minisat-temp >> Ramsey_5_5_2_${n}_SB_MC.cnf.result.minisat2;rm -f Ramsey_5_5_2_${n}{,_SB_MC}.{e,}cnf" >> experiments;
        echo "MARCH_PL_MC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_MC_${n}.ecnf > Ramsey_5_5_2_${n}_SB_MC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_MC.ecnf > Ramsey_5_5_2_${n}_SB_MC.cnf && ./solvers/march_pl Ramsey_5_5_2_${n}_SB_MC.cnf > Ramsey_5_5_2_${n}_SB_MC.cnf.result.march_pl 2>&1;rm -f Ramsey_5_5_2_${n}{_SB_MC,}.{e,}cnf" >> experiments;
        echo "OKSOLVER_MC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_MC_${n}.ecnf > Ramsey_5_5_2_${n}_SB_MC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_MC.ecnf > Ramsey_5_5_2_${n}_SB_MC.cnf && ./solvers/OKsolver_2002-O3-DNDEBUG -O -D20 -M -F Ramsey_5_5_2_${n}_SB_MC.cnf > Ramsey_5_5_2_${n}_SB_MC.cnf.result.OKsolver 2>&1; mv Ramsey_5_5_2_${n}_SB_MC.cnf.mo Ramsey_5_5_2_${n}_SB_MC.cnf.mo.OKsolver;mv Ramsey_5_5_2_${n}_SB_MC.cnf.pa Ramsey_5_5_2_${n}_SB_MC.cnf.pa.OKsolver;rm -f Ramsey_5_5_2_${n}{,_SB_MC}.{e,}cnf" >> experiments;
        echo "OKSOLVERM2PP_MC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_MC_${n}.ecnf > Ramsey_5_5_2_${n}_SB_MC.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_MC.ecnf > Ramsey_5_5_2_${n}_SB_MC.cnf && ./solvers/OKsolver_2002-m2pp -O -D20 -M -F Ramsey_5_5_2_${n}_SB_MC.cnf > Ramsey_5_5_2_${n}_SB_MC.cnf.result.OKsolver-m2pp 2>&1; mv Ramsey_5_5_2_${n}_SB_MC.cnf_m2pp_*.mo Ramsey_5_5_2_${n}_SB_MC.cnf.mo.OKsolver-m2pp;mv Ramsey_5_5_2_${n}_SB_MC.cnf_m2pp_*.pa Ramsey_5_5_2_${n}_SB_MC.cnf.pa.OKsolver-m2pp;rm -f Ramsey_5_5_2_${n}{,_SB_MC}.{e,}cnf" >> experiments;
    # Symmetry breaking 3
       echo "PICOSAT_PHP"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_PHP_${n}.ecnf > Ramsey_5_5_2_${n}_SB_PHP.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_PHP.ecnf > Ramsey_5_5_2_${n}_SB_PHP.cnf && ./solvers/picosat913 -v Ramsey_5_5_2_${n}_SB_PHP.cnf > Ramsey_5_5_2_${n}_SB_PHP.cnf.result.picosat 2>&1 && rm -f Ramsey_5_5_2_${n}{,_SB_PHP}.{e,}cnf" >> experiments;
        echo "MINISAT2_PHP"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_PHP_${n}.ecnf > Ramsey_5_5_2_${n}_SB_PHP.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_PHP.ecnf > Ramsey_5_5_2_${n}_SB_PHP.cnf && ./solvers/minisat2 Ramsey_5_5_2_${n}_SB_PHP.cnf minisat-temp > Ramsey_5_5_2_${n}_SB_PHP.cnf.result.minisat2 2>&1; cat minisat-temp >> Ramsey_5_5_2_${n}_SB_PHP.cnf.result.minisat2;rm -f Ramsey_5_5_2_${n}{,_SB_PHP}.{e,}cnf" >> experiments;
        echo "MARCH_PL_PHP"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_PHP_${n}.ecnf > Ramsey_5_5_2_${n}_SB_PHP.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_PHP.ecnf > Ramsey_5_5_2_${n}_SB_PHP.cnf && ./solvers/march_pl Ramsey_5_5_2_${n}_SB_PHP.cnf > Ramsey_5_5_2_${n}_SB_PHP.cnf.result.march_pl 2>&1;rm -f Ramsey_5_5_2_${n}{_SB_PHP,}.{e,}cnf" >> experiments;
        echo "OKSOLVER_PHP"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_PHP_${n}.ecnf > Ramsey_5_5_2_${n}_SB_PHP.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_PHP.ecnf > Ramsey_5_5_2_${n}_SB_PHP.cnf && ./solvers/OKsolver_2002-O3-DNDEBUG -O -D20 -M -F Ramsey_5_5_2_${n}_SB_PHP.cnf > Ramsey_5_5_2_${n}_SB_PHP.cnf.result.OKsolver 2>&1; mv Ramsey_5_5_2_${n}_SB_PHP.cnf.mo Ramsey_5_5_2_${n}_SB_PHP.cnf.mo.OKsolver;mv Ramsey_5_5_2_${n}_SB_PHP.cnf.pa Ramsey_5_5_2_${n}_SB_PHP.cnf.pa.OKsolver;rm -f Ramsey_5_5_2_${n}{,_SB_PHP}.{e,}cnf" >> experiments;
        echo "OKSOLVERM2PP_PHP"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} > Ramsey_5_5_2_${n}.ecnf && ./merge_cnf.sh Ramsey_5_5_2_${n}.ecnf Ramsey_SB_PHP_${n}.ecnf > Ramsey_5_5_2_${n}_SB_PHP.ecnf && ./ExtendedToStrictDimacs-O3-DNDEBUG < Ramsey_5_5_2_${n}_SB_PHP.ecnf > Ramsey_5_5_2_${n}_SB_PHP.cnf && ./solvers/OKsolver_2002-m2pp -O -D20 -M -F Ramsey_5_5_2_${n}_SB_PHP.cnf > Ramsey_5_5_2_${n}_SB_PHP.cnf.result.OKsolver-m2pp 2>&1; mv Ramsey_5_5_2_${n}_SB_PHP.cnf_m2pp_*.mo Ramsey_5_5_2_${n}_SB_PHP.cnf.mo.OKsolver-m2pp;mv Ramsey_5_5_2_${n}_SB_PHP.cnf_m2pp_*.pa Ramsey_5_5_2_${n}_SB_PHP.cnf.pa.OKsolver-m2pp;rm -f Ramsey_5_5_2_${n}{,_SB_PHP}.{e,}cnf" >> experiments;
    # Cardinality Constraints
       echo "PICOSAT_CC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./merge_cnf.sh Card/Card_n${n}.cnf Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}_CC.cnf && ./solvers/picosat913 -v Ramsey_5_5_2_${n}_CC.cnf > Ramsey_5_5_2_${n}_CC.cnf.result.picosat 2>&1 && rm -f Ramsey_5_5_2_${n}{,_CC}.{e,}cnf" >> experiments;
        echo "MINISAT2_CC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./merge_cnf.sh Card/Card_n${n}.cnf Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}_CC.cnf && ./solvers/minisat2 Ramsey_5_5_2_${n}_CC.cnf minisat-temp > Ramsey_5_5_2_${n}_CC.cnf.result.minisat2 2>&1; cat minisat-temp >> Ramsey_5_5_2_${n}_CC.cnf.result.minisat2;rm -f Ramsey_5_5_2_${n}{,_CC}.{e,}cnf" >> experiments;
        echo "OKSOLVER_CC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./merge_cnf.sh Card/Card_n${n}.cnf Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}_CC.cnf && ./solvers/OKsolver_2002-O3-DNDEBUG -O -D20 -M -F Ramsey_5_5_2_${n}_CC.cnf > Ramsey_5_5_2_${n}_CC.cnf.result.OKsolver 2>&1; mv Ramsey_5_5_2_${n}_CC.cnf.mo Ramsey_5_5_2_${n}_CC.cnf.mo.OKsolver;mv Ramsey_5_5_2_${n}_CC.cnf.pa Ramsey_5_5_2_${n}_CC.cnf.pa.OKsolver;rm -f Ramsey_5_5_2_${n}{,_CC}.{e,}cnf" >> experiments;
        echo "OKSOLVERM2PP_CC"$n "./Ramsey-O3-DNDEBUG 5 5 2 ${n} | ./ExtendedToStrictDimacs-O3-DNDEBUG > Ramsey_5_5_2_${n}.cnf && ./merge_cnf.sh Card/Card_n${n}.cnf Ramsey_5_5_2_${n}.cnf > Ramsey_5_5_2_${n}_CC.cnf && ./solvers/OKsolver_2002-m2pp -O -D20 -M -F Ramsey_5_5_2_${n}_CC.cnf > Ramsey_5_5_2_${n}_CC.cnf.result.OKsolver-m2pp 2>&1; mv Ramsey_5_5_2_${n}_CC.cnf_m2pp_*.mo Ramsey_5_5_2_${n}_CC.cnf.mo.OKsolver-m2pp;mv Ramsey_5_5_2_${n}_CC.cnf_m2pp_*.pa Ramsey_5_5_2_${n}_CC.cnf.pa.OKsolver-m2pp;rm -f Ramsey_5_5_2_${n}{,_CC}.{e,}cnf" >> experiments;
    done
       
  • The above experiment (in the generation script) is currently running on cspasiphae with a timeout of 2 hours.
  • Combining all such investigations (different symmetry breaking techniques, cardinality contraints etc) into a single experiment allows one to run through all such investigations for a short time and then split the experiments if certain aspects are slowing the entire experiment set down or it makes more sense to run certain parts, or solvers in parallel.
Todo:
Using UBCSAT
  • The list of algorithms from ubcsat:
    1. "ubcsat-okl -alg gsat -runs 100 -i Ramsey_5_2_n.cnf": trivial for n=30; n = 35 needs 300 - 30000 steps. Using "-cutoff 2000" seems reasonable.
    2. gwsat: trivial for n=30; n = 35 ?
    3. hsat: n = 35 needs ~ 3000 steps; n = 40 ?
    4. adaptnovelty+: n = 35 ?
    5. saps: n = 35 in 600 steps. Using "-cutoff 2000" seems reasonable; looks strong. n = 40 ?
    6. rsaps: similar; but looks bleak for n = 40 (cutoffs 10000 or 30000 yield nearly the same).
    7. samd performs yet best, and also scales to higher cutoffs, but very slowly: With n=40, cutoff = 10 000 000, in 12 rounds 9 outcomes were 30-something, one was 46, and we had 23 (the minimum) and 27 (regarding the falsified clauses).
  • Investigating samd:
    1. n=35 very easy.
    2. n=38:
      > ubcsat-okl -alg samd -cutoff 20000 -runs 10000 -i Ramsey_5_5_2_38.cnf > Exp_Ramsey_5_5_2_38
      Clauses = 1003884
      Variables = 703
      TotalLiterals = 10038840
      FlipsPerSecond = 800    
      BestStep_Mean = 11197.468000
      Steps_Mean = 20000.000000
      Steps_Max = 20000.000000
      PercentSuccess = 0.00  
      BestSolution_Mean = 16.367800
      BestSolution_Median = 16.000000
      BestSolution_Min = 7.000000
      BestSolution_Max = 51.000000
           
      We need to investigate the distribution of falsified clauses reached, using R.
    3. Summary:
      > E = read.table("Exp_Ramsey_5_5_2_38", colClasses = c("character", "factor", "integer", "integer", "integer", "character"))
      > summary(E)
       sat            min            osteps   
       0:10000   Min.   : 7.00   Min.   :  166
                 1st Qu.:14.00   1st Qu.: 6576
                 Median :16.00   Median :11372
                 Mean   :16.37   Mean   :11197
                 3rd Qu.:18.00   3rd Qu.:16167
                 Max.   :51.00   Max.   :20000
           
    4. > plot(min ~ osteps, data = E)
           
      shows that there is a strong correlation between the worst min-values and the smallest osteps-values, but then the correlation gets much weaker (and the largest osteps-value include also some rather bad cases (without much improvement).
    5. Frequencies of min-values:
      > table(E$min)
      
         7    8    9   10   11   12   13   14   15   16   17   18   19   20   21   22
         1    4   21   72  181  410  798 1236 1545 1598 1315 1007  621  413  238  130
      
        23   24   25   26   27   28   29   30   31   32   33   34   35   36   37   38
        94   65   63   43   28   26   14   14   19    2    9    3    4    1    1    6
      
        39   40   41   42   43   44   45   47   50   51
         3    2    1    1    2    2    4    1    1    1
           
      concentrates around the mean, but with a long tail.
    6. Frequencies of osteps-values:
      > hist(E$osteps, plot=F)
      $breaks
       [1]     0  1000  2000  3000  4000  5000  6000  7000  8000  9000 10000 11000
      [13] 12000 13000 14000 15000 16000 17000 18000 19000 20000
      
      $counts
       [1] 133 277 382 449 476 498 516 518 510 531 512 541 527 534 500 511 581 594 679
      [20] 731
           
    7. For cutoff = 40000:
      Clauses = 1003884
      Variables = 703
      TotalLiterals = 10038840
      FlipsPerSecond = 1273   
      BestStep_Mean = 20416.061900
      Steps_Mean = 40000.000000
      Steps_Max = 40000.000000
      PercentSuccess = 0.00  
      BestSolution_Mean = 14.926500
      BestSolution_Median = 15.000000
      BestSolution_Min = 4.000000
      BestSolution_Max = 51.000000
           
    8. There is now more data available ("Exp_Ramsey_5_5_2_38-samd_40000_2") which needs to be merged with the old data (and then the evaluation needs to be repeated).
    9. The density of osteps has a clear minimum at around 20000, while the minimum 4 is reached for osteps = 34213. Linear modelling via L = lm(min ~ poly(log(osteps), k),data=E) makes sense up to k=4 (plotting by
      plot(log(E$osteps),E$min)
      points(log(E$osteps),predict(L),col="blue")
           
      shows a reasonable fit).
    10. For cutoff = 80000:
      ubcsat-okl -alg samd -cutoff 80000 -runs 10000 -i Ramsey_5_5_2_38.cnf > Exp_Ramsey_5_5_2_38_80000
      Clauses = 1003884
      Variables = 703
      TotalLiterals = 10038840
      FlipsPerSecond = 3404   
      BestStep_Mean = 35709.517200
      Steps_Mean = 80000.000000
      Steps_Max = 80000.000000
      PercentSuccess = 0.00  
      BestSolution_Mean = 13.943300
      BestSolution_Median = 13.000000
      BestSolution_Min = 4.000000
      BestSolution_Max = 56.000000
           
    11. Also experimental results for a 10x larger experiments are available (the above smaller experiment should be merged into the larger one).
      Clauses = 1003884
      Variables = 703
      TotalLiterals = 10038840
      FlipsPerSecond = 3470   
      BestStep_Mean = 35903.717040
      Steps_Mean = 80000.000000
      Steps_Max = 80000.000000
      PercentSuccess = 0.00  
      BestSolution_Mean = 13.908400
      BestSolution_Median = 13.000000
      BestSolution_Min = 1.000000
      BestSolution_Max = 67.000000
           
    12. Basically the same picture as for cutoff = 20000; the main question here is which questions to ask??
    13. It seems reasonable to consider log(osteps) instead of osteps; plot(min ~ log(osteps), data = E) shows then a clear negative correlation, but where, due to the "cutoff effect", the minimum is reached already at around osteps = 63000 (not with 80000).
    14. It seems that the density of osteps reaches its minimum also around osteps = 63000?! (use hist(E$osteps,breaks=50))
    15. This seems reasonable: The higher osteps the better the result but the harder to get there, except of the "cutoff-effect", which makes very high osteps-values more likely but less fruitful.
    16. Using here log(osteps) doesn't seem sensible: plot(density(E$osteps),lab=c(10,5,7)) shows the minimum density somewhat below 60000, while plot(density(log(E$osteps)),lab=c(10,5,7)) has its maximum* around exp(11) ~ 60000.
    17. n=40:
      1. cutoff = 10 000 000 and noimprove = 1 000 000: 100 rounds, maximum 3 500 000 steps, average 1 700 000 steps, minimum 7 falsified clauses.
      2. cutoff = 20 000 000, noimprove = 3 000 000: 100 rounds, maximum 10 500 000 steps, average 4 300 000 steps, minimum 1 falsified clause (seed 18745606).
      3. One round, cutoff = 20 000 000, with previous best seed: didn't improve the result.
      4. So let's try 500 runs, with cutoff = 20 000 000, noimprove = 2 000 000:
        BestStep_Mean = 1121189.316000
        Steps_Mean = 3121190.316000
        Steps_Max = 7623900.000000
        PercentSuccess = 0.00
        BestSolution_Mean = 34.696000
        BestSolution_Median = 35.000000
        BestSolution_Min = 7.000000
        BestSolution_Max = 76.000000
               
      5. Alright, with noimprove = 3 000 000:
        1. BestStep_Mean = 1596309.594000
          Steps_Mean = 4590310.592000
          Steps_Max = 14784949.000000
          PercentSuccess = 0.20
          BestSolution_Mean = 33.976000
          BestSolution_Median = 35.000000
          BestSolution_Min = 0.000000
          BestSolution_Max = 61.000000
                   
        2. With seed = 391532901 a solution was found (in round 293, using 964281 steps)!
          • The command line instruction to reproduce this is:
            ubcsat -alg samd -seed 391532901 -cutoff 1000000 -i Ramsey_5_2_40.cnf
                       
          • A solution is output by adding "-solve".
          • Perhaps this solution should be stored; the question is where? Perhaps this is similar to data for minimally unsatisfiable clause-sets etc., which finally is too much to put into source control, but should exist as additional packages.
          • Of course, there is the whole complex of "database questions"; see Experimentation/Database/plans/general.hpp
          • We need to find out whether this solution is of interest (i.e., "unknown") or not.
          • So we need to find out about the known solutions for n=40 in the literature, and about classifications of solutions (when solutions are considered to be the "same").
        3. So, in general perhaps one should just use a cutoff of 1 000 000, and use more rounds?
    18. n=41:
      1. cutoff = 10 000 000, with 40 rounds most results were fiftyish to sixtyish, but one outlier reached 28 (the minimum).
      2. cutoff = 20 000 000, noimprove = 2 000 000: 100 rounds has a maximum of 8 000 000 steps, average of 3 300 000 steps, and 2261 flips per second. The optimum reached was 13 falsified clauses, which seems very good.
      3. noimprove = 3 000 000: 100 rounds, maximum 12 600 000 steps, average 5 000 000 steps, 2294 flips per second, minimum 12 falsified clauses (seed 1833218426)
      4. One round, cutoff = 20 000 000, with previous best seed: didn't improve the result.
      5. So let's try cutoff = 20 000 000, noimprove = 3 000 000.
        > ubcsat-okl -alg samd -cutoff 20000000 -noimprove 3000000 -runs 100 -i Ramsey_5_5_2_41.cnf
               Clauses = 1498796
        Variables = 820
        TotalLiterals = 14987960
        FlipsPerSecond = 552
        BestStep_Mean = 2271951.410000
        Steps_Mean = 5271952.410000
        Steps_Max = 14351275.000000
        PercentSuccess = 0.00
        BestSolution_Mean = 54.470000
        BestSolution_Median = 56.000000
        BestSolution_Min = 1.000000
        BestSolution_Max = 70.000000
               
        (the best solution was found with the maximum number of steps).
      6. Removing the noimprove-value, actually a solution was found:
        > ubcsat-okl -alg samd -cutoff 20000000 -runs 100 -i Ramsey_5_5_2_41.cnf
              1 0    54     387633   20000000  451534902
              2 0    55    4031001   20000000 2277530380
              3 1     0   17699250   17699250  147704963
               
        Was this pure chance? (By the way, that was using ubcsat-1.1.0, and we should check whether the seed is the same for 1.0.0.)
    19. n=42
      1. On cscharon (64 bit, ubcsat version 1.1.0):
        > ubcsat-okl -alg samd -cutoff 20000000 -runs 100 -i Ramsey_5_5_2_42.cnf
               
        on 7 runs minimum was 77, maximum 86 falsified clauses.
      2. 500 runs with a cutoff 100000 yields between 83 and 107 falsified clauses: Initially it's very easy, but then improvement is very hard, and only very few runs are better --- but then they are much better, while the rest is very close together. We need better data:
        1. cutoff = 1000, 5000 runs:
          Clauses = 1701336
          Variables = 861
          TotalLiterals = 17013360
          FlipsPerSecond = 1938
          BestStep_Mean = 875.772200
          Steps_Mean = 1000.000000
          Steps_Max = 1000.000000
          PercentSuccess = 0.00
          BestSolution_Mean = 130.212200
          BestSolution_Median = 130.000000
          BestSolution_Min = 108.000000
          BestSolution_Max = 160.000000
                   
          cutoff = 10000, 5000 runs: (cs-wsok)
          Clauses = 1701336
          Variables = 861
          TotalLiterals = 17013360
          FlipsPerSecond = 2276
          BestStep_Mean = 7167.124200
          Steps_Mean = 10000.000000
          Steps_Max = 10000.000000
          PercentSuccess = 0.00
          BestSolution_Mean = 106.278800
          BestSolution_Median = 106.000000
          BestSolution_Min = 85.000000
          BestSolution_Max = 126.000000
                   
        2. Alternatively with gsat-tabu:
          > ubcsat-okl -alg gsat-tabu -i Ramsey_5_5_2_42.cnf -runs 5000 -cutoff 10000
          Clauses = 1701336
          Variables = 861
          TotalLiterals = 17013360
          FlipsPerSecond = 1721
          BestStep_Mean = 7232.085000
          Steps_Mean = 10000.000000
          Steps_Max = 10000.000000
          PercentSuccess = 0.00
          BestSolution_Mean = 105.163400
          BestSolution_Median = 105.000000
          BestSolution_Min = 85.000000
          BestSolution_Max = 124.000000
                   
          Might be slightly better, but seems to be quite a bit slower.
        3. cutoff = 100,000, 5000 runs: (cs-wsok)
          Clauses = 1701336
          Variables = 861
          TotalLiterals = 17013360
          FlipsPerSecond = 2010
          BestStep_Mean = 59262.030800
          Steps_Mean = 100000.000000
          Steps_Max = 100000.000000
          PercentSuccess = 0.00
          BestSolution_Mean = 94.735400
          BestSolution_Median = 95.000000
          BestSolution_Min = 82.000000
          BestSolution_Max = 111.000000
                   
          only a bit progress.
        4. Alternatively with gsat-tabu:
          Clauses = 1701336
          Variables = 861
          TotalLiterals = 17013360
          FlipsPerSecond = 1646
          BestStep_Mean = 59331.269400
          Steps_Mean = 100000.000000
          Steps_Max = 100000.000000
          PercentSuccess = 0.00
          BestSolution_Mean = 93.784200
          BestSolution_Median = 94.000000
          BestSolution_Min = 75.000000
          BestSolution_Max = 143.000000
                   
          might have a higher variability?
        5. cutoff = 1,000,000, 500 runs: (cscarme)
          Clauses = 1701336
          Variables = 861
          TotalLiterals = 17013360
          FlipsPerSecond = 2135
          BestStep_Mean = 477504.9
          Steps_Mean = 1000000
          /compsci/saturn/staff/csoliver/OKplatform/bin/ubcsat-okl: line 12: 26989 Segmentation fault
                   
          where the data was then analysed using R, copying the output to a file "ExpRamsey1000000" starting like
          sat min osteps msteps seed
                1 0    90     153638    1000000 1649159937
                2 0    92     284850    1000000 1886480441
                3 0    86     636866    1000000 2139335150
                   
          and where then analysis is very simple, e.g.
          R1 = read.table("ExpRamsey1000000")
          > min(R1$min)
          [1] 77
          > max(R1$min)
          [1] 106
          > median(R1$min)
          [1] 88
          > mean(R1$min)
          [1] 87.8
                   
          we see, again very little progress.
        6. cutoff = 10,000,000, 500 runs (cs-wsok)
        7. cutoff = 40,000,000, 50 runs (cscharon)
    20. n=43:
      1. Also if this is unsatisfiable, one would only expect gradual differences compared to n=42 for local-search algorithms.
      2. cutoff = 10,000,000, 50 runs (csoberon)
        Clauses = 1925196
        Variables = 903
        TotalLiterals = 19251960
        FlipsPerSecond = 1947
        BestStep_Mean = 4888045.6
        Steps_Mean = 10000000
        /compsci/saturn/staff/csoliver/OKplatform/bin/ubcsat-okl: line 12:  9651 Segmentation fault
               
        and furthermore
        > min(R2$min)
        [1] 112
        > max(R2$min)
        [1] 126
        > median(R2$min)
        [1] 117.5
        > mean(R2$min)
        [1] 117.38
               
      3. cutoff = 100,000,000, 50 runs (csoberon)

Definition in file Ramsey_2_5_5.hpp.