2018年8月20日月曜日

新しい解の発見 その2

性懲りもなく、未だ研究していて、その甲斐あって

instance20の新解を発見しました。


 So Far Bestknown New Solution  
 LBUBLBUB
Instance153823383438243831
Instance204743494347694778

2018年8月15日水曜日

116Aをリリースしました

エンジンは、変更していません。来年2/3月の勤務表を作る必要がある、という放射線関係のReq.にお応えして、2019年のカレンダをEnableしました。(本Versionよりライセンスドユーザは、2100年までEnableしています。)

また、UserContributionsということで、下記のサンプルを追加しています。

2交代診療所
・正循環
・複数の介護施設

特に複数の介護施設は、込み入っているので後で解説を書こうと思います。



2018年8月8日水曜日

マルチスレッド化検討

今回は、OpenMPを使おうと思っています。今回の技術開発において、最後の仕上げという段階に来て、OpenMPの調査を開始しました。小規模のソースの場合、数秒ですのであまり意味はないのですが、大規模ベンチマークテストでは、数十時間も走らせるので意味があります。開発マシンもメモリを増強し48GBとしました。

2018年7月29日日曜日

インテルのNadelさんから、コンパイルできないご指摘を頂きました


I’m getting errors concerning PRIi64: the compiler can’t recognize it. I’ve tried various compilers, but with no luck:
../MapleSAT/utils/Options.h: In member function ‘virtual void Minisat::Int64Option::help(bool)’:
../MapleSAT/utils/Options.h:285:29: error: unable to find string literal operator ‘operator""PRIi64’ with ‘const char [3]’, ‘long unsigned int’ arguments
            fprintf(stderr, "%4"PRIi64, range.begin);
Have you encountered such problems? Which compiler did you use?

私の開発環境は、VisualStudio2015で、Linuxは、あまり経験がないのですが、BashOnWindowsでポートしました。次のログのようにコンパイルは出来ました。

I'm sorry for nasty codes.
Originally, I wrote it using Visutal Studio 2015. After that, I moved the project into linux environment using bash on ubuntu on Windows.
This was a year ago.
Now,I successfully compiled it per following log.
Some g++ version may affect the compilation error.

taksugawara@win10-64:/mnt/c/cygwin64/home/tak.sugawara/MSE2018/maxroster/maxroster/code/linux$ ls
Makefile
taksugawara@win10-64:/mnt/c/cygwin64/home/tak.sugawara/MSE2018/maxroster/maxroster/code/linux$ g++ --version
g++ (Ubuntu 5.4.0-6ubuntu1~16.04.4) 5.4.0 20160609
Copyright (C) 2015 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
taksugawara@win10-64:/mnt/c/cygwin64/home/tak.sugawara/MSE2018/maxroster/maxroster/code/linux$ make clean
rm -rf ../MapleSAT/core/Solver.o ../maxsat3.o ../oll.o ../oll2.o ../inc_maxsat.o ../sat_search.o ../Ramp-master/ramp.o ../MapleSAT/simp/SimpSolver.o ../wpm3_inc.o ../unweight.o ../main_maxsat.o ../oll2_seq.o ../oll2_inc.o ../../bin/maxroster
taksugawara@win10-64:/mnt/c/cygwin64/home/tak.sugawara/MSE2018/maxroster/maxroster/code/linux$ make
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../MapleSAT/core/Solver.cpp -o ../MapleSAT/core/Solver.o
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../maxsat3.cpp -o ../maxsat3.o
In file included from ../maxsat.h:19:0,
                 from ../maxsat3.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../maxsat3.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
../maxsat3.cpp: At global scope:
../maxsat3.cpp:1096:26: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  const int buffer_size = 10000;
                          ^
../maxsat3.cpp: In member function ‘uint64_t Minisat::MaxSAT::non_repeat_search(std::set<Minisat::Lit>&)’:
../maxsat3.cpp:2062:97: warning: format ‘%zd’ expects argument of type ‘signed size_t’, but argument 3 has type ‘int’ [-Wformat=]
  printf("c weights=%zd longest=%zd new weight=%zd \n", weight_map.size(), longest, highet_weight);
                                                                                                 ^
../maxsat3.cpp:2077:45: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘uint64_t {aka long unsigned int}’ [-Wformat=]
    printf("c new weight=%d\n", highet_weight);
                                             ^
../maxsat3.cpp: In function ‘void Minisat::printStats1(Minisat::Solver&)’:
../maxsat3.cpp:2722:58: warning: format ‘%lld’ expects argument of type ‘long long int’, but argument 2 has type ‘uint64_t {aka long unsigned int}’ [-Wformat=]
  printf("c restarts              : %lld\n", solver.starts);
                                                          ^
../maxsat3.cpp:2723:63: warning: format ‘%lld’ expects argument of type ‘long long int’, but argument 2 has type ‘uint64_t {aka long unsigned int}’ [-Wformat=]
  printf("c conflicts             : %lld  \n", solver.conflicts);
                                                               ^
../maxsat3.cpp:2724:63: warning: format ‘%lld’ expects argument of type ‘long long int’, but argument 2 has type ‘uint64_t {aka long unsigned int}’ [-Wformat=]
  printf("c decisions             : %lld  \n", solver.decisions);
                                                               ^
../maxsat3.cpp:2725:66: warning: format ‘%lld’ expects argument of type ‘long long int’, but argument 2 has type ‘uint64_t {aka long unsigned int}’ [-Wformat=]
  printf("c propagations          : %lld  \n", solver.propagations);
                                                                  ^
../maxsat3.cpp:2726:166: warning: format ‘%lld’ expects argument of type ‘long long int’, but argument 2 has type
uint64_t {aka long unsigned int}’ [-Wformat=]
 %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals) * 100 / (double)solver.max_literals);
                                                                                                                     ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../oll.cpp -o ../oll.o
In file included from ../maxsat.h:19:0,
                 from ../oll.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../oll.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../oll2.cpp -o ../oll2.o
In file included from ../maxsat.h:19:0,
                 from ../oll2.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../oll2.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../inc_maxsat.cpp -o ../inc_maxsat.o
In file included from ../maxsat.h:19:0,
                 from ../inc_maxsat.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../inc_maxsat.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../sat_search.cpp -o ../sat_search.o
In file included from ../maxsat.h:19:0,
                 from ../sat_search.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../sat_search.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../Ramp-master/ramp.cpp -o ../Ramp-master/ramp.o
In file included from ../Ramp-master/myHeap.h:5:0,
                 from ../Ramp-master/ramp.cpp:15:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../Ramp-master/ramp.cpp:18:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
../Ramp-master/ramp.cpp: In member function ‘int RAMP::Ramp::build_instance(char*)’:
../Ramp-master/ramp.cpp:237:86: warning: format ‘%lld’ expects argument of type ‘long long int*’, but argument 7 has type ‘LL* {aka long int*}’ [-Wformat=]
  sscanf(line, "%s %s %d %d %lld", tempstr1, tempstr2, &var_n, &clause_n, &weight_hard);
                                                                                      ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../MapleSAT/simp/SimpSolver.cpp -o ../MapleSAT/simp/SimpSolver.o
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../wpm3_inc.cpp -o ../wpm3_inc.o
In file included from ../maxsat.h:19:0,
                 from ../wpm3_inc.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../wpm3_inc.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../unweight.cpp -o ../unweight.o
In file included from ../maxsat.h:19:0,
                 from ../unweight.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../unweight.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../main_maxsat.cpp -o ../main_maxsat.o
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../oll2_seq.cpp -o ../oll2_seq.o
In file included from ../maxsat.h:19:0,
                 from ../oll2_seq.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../oll2_seq.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
../oll2_seq.cpp: In member function ‘void Minisat::MaxSAT::oll2_search_oll_mcu3(uint64_t)’:
../oll2_seq.cpp:768:32: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘uint64_t {aka long unsigned int}’ [-Wformat=]
      printf("c cost=%d\n", cost);
                                ^
g++ -c  -fopenmp  -O3  -I../MapleSAT -I../ -I../Ramp-master ../oll2_inc.cpp -o ../oll2_inc.o
In file included from ../maxsat.h:19:0,
                 from ../oll2_inc.cpp:14:
../Ramp-master/ramp.h:49:13: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
  int seed = 10;;
             ^
../Ramp-master/ramp.h:60:25: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 const int print_speed = 50000;
                         ^
../Ramp-master/ramp.h:62:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int answer_writed = 0;
                     ^
../Ramp-master/ramp.h:64:21: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int flag_weighted = 0;
                     ^
../Ramp-master/ramp.h:68:14: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int greedy = 1;
              ^
../Ramp-master/ramp.h:72:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  max_flips = 20000000000000ll;
                 ^
../Ramp-master/ramp.h:73:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL flip_bound = 0;
                 ^
../Ramp-master/ramp.h:74:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL  step = 1;
            ^
../Ramp-master/ramp.h:75:12: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie = 1;
            ^
../Ramp-master/ramp.h:105:20: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 double time_best = 0;
                    ^
../Ramp-master/ramp.h:106:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 LL step_best = 0;
                ^
../Ramp-master/ramp.h:107:17: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int trie_best = 0;
                 ^
../Ramp-master/ramp.h:113:10: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int p1 = 6000;
          ^
../Ramp-master/ramp.h:114:16: warning: non-static data member initializers only available with -std=c++11 or -std=gnu++11
 int init_try = 1;
                ^
In file included from ../oll2_inc.cpp:14:0:
../maxsat.h:149:3: warning: ‘typedef’ was ignored in this declaration
  };
   ^
../maxsat.h: In member function ‘void Minisat::TNode::print()’:
../maxsat.h:196:20: warning: format ‘%x’ expects argument of type ‘unsigned int’, but argument 2 has type ‘Minisat::TNode*’ [-Wformat=]
   printf("%x", this);
                    ^
../maxsat.h:199:31: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘Minisat::Lit’ [-Wformat=]
    printf("%d ", linkingVar[i]);
                               ^
g++  ../MapleSAT/core/Solver.o ../maxsat3.o ../oll.o ../oll2.o ../inc_maxsat.o ../sat_search.o ../Ramp-master/ramp.o ../MapleSAT/simp/SimpSolver.o ../wpm3_inc.o ../unweight.o ../main_maxsat.o ../oll2_seq.o ../oll2_inc.o -o ../../bin/maxroster -lpthread -fopenmp -lz -lrt -static
taksugawara@win10-64:/mnt/c/cygwin64/home/tak.sugawara/MSE2018/maxroster/maxroster/code/linux$

Best Regards,
Tak.Sugawara

2018年7月26日木曜日

特許料を納め過ぎたときに届くものは?

過誤納のお知らせ

xxx様

下記の特許料(登録料)納付手続きについて、過誤納が生じております。過誤納分は、請求により返還致します..

というお知らせが特許庁より届きました。78,940円のところ、78,960円納め、過誤納額は、20円でした。

どこで計算をミスったかは分かりませんでしたが、納めすぎた方向でよかったです。 返還請求は、任意ですので、ほっておいてもなにも問題ないです。(請求する場合は1年以内)

2018年7月22日日曜日

MAXSAT Evaluation 2018結果

各ソルバーの実装内容については、こちら
https://helda.helsinki.fi/bitstream/handle/10138/237139/mse18_proceedings.pdf?sequence=1

結果については、こちら
https://maxsat-evaluations.github.io/2018/mse18-talk.pdf

今年は、2位が2トラック、3位が1トラックという結果になりました。前にも書いたように、今年は提出していないので、去年のソルバーでの結果です。

コンペは、Complete部門とInCompleteに分かれています。Completeは、厳密解を競うものです。去年は、HittingSetを用いたHybridソルバーが強かったのですが、今年は、Unsatベースが1位で、意外な結果となりました。
WeightにおけるカクタスプロットのVBSは、Virtual_Best_Solverです。各ソルバー方式、得意なインスタンスが違うのですが、仮想的に、全部の良いところだけを取ってきたソルバーだったら、どうなるかということを示しています。このカクタスプロットを見ると相当開きがあるので、
インスタンス毎に、ソルバーを切り替えれば、VBSのところまで、性能を向上させることが出来るということを示しています。万能な方式があればなにも苦労はしないのですが、 最近の論文の潮流は、要素技術の深化とともに、既存の手法を以下に上手に切り替えるか、ということもあると思います。
下は、上記資料よりの引用で、この10年での性能向上推移です。MaxSAT Communityの方々に頭が下がる思いです。



2018年7月15日日曜日

SAT competition 結果

http://sat2018.forsyte.tuwien.ac.at/downloads/satcomp18slides.pdf

で結果が出ています。やはり上位は、MapleSAT系で占められており、一昨年の登場以来、確固たる潮流を感じます。mainトラックの1位は、前に紹介したNadelさんです。

2018年7月12日木曜日

プレゼンを更新しました

http://www.nurse-scheduling-software.com/publications/presentation_for_hospitals2018.pdf

この資料を見られてかどうかは、知りませんが問い合わせが急に多くなりました。

嘘は、書いていませんが、未だ、目指すところが出来ていないので心苦しいのです。PythonによるDSL(Domain Specific Language)実装が出来たところで、SEさんに腕を奮って頂けると思いますが、先は長いです。

自分は、パナファコムで、FDDの評価をした後、アルプス電気で、基板設計・FDD設計・LSI屋、高周波を少し勉強した後、退社して、その後は、VerilogHDLのコンパイラを書いていました。

言語実装手法もLex/Yaccの時代から変わってきています。この辺は、オープンソースにしてブログで実装を書いていきたいと思います。

2018年7月11日水曜日

商標登録証が届きました インテリナビ

ベンチマーク20-24は、超難問

どうしても、解けなくて悩んでいます。7種の解法を新しく考案したのですが、20を除いて、撃沈してしまいました。最後に、もう一種、考案したので、そちらを試して駄目だったら、いい加減にまとめに入ろうかと思います。 この一年、色々学ぶことが出来て幸せでした。ほとんどフルタイムで、考えることに没頭できました。大学の先生に聞くと、9割ぐらいは、雑用で取られるようなので、頭の悪さを差っぴいても私の方が有利です。この年になると、忘却との戦いが始まるのですが、それでも、未だ色々アイデアは出てくるものだなあ、と我ながら感心します。

新しく購入した本は、
・The Art Of Computer Programming 4A
・繁野麻衣子先生の数理最適化

です。4Aは、有名なKnuth大先生が何十年にも渡って書かれている著作の一部です。そのためにLatexを作ったというのは、有名な話しらしいです。いくつかの参照した論文で言及されていたので、確かめるために買ったのですが、ちょっと今のところ出番はなさそうです。

CuttingPlaneのアプローチは、日本語の文献がほとんどなく、この本(数理最適化)でも僅かしか記述されていませんでしたが、入門的には、十分役に立ちました。むしろ、組み合わせ最適化という分野に突入するまえに、一番最初に読みべき本でした。麻衣子先生は、おちゃめな先生で教わりたかったです。なぜか、この分野の研究者は、女性が多いのですが、どうしてなんでしょうね。 

2018年6月23日土曜日

引用されています。その2

MaxSAT2018関連で、また引用されています。

https://arxiv.org/pdf/1806.07164.pdf

インド工科大学のSaurabh Joshiさんの論文に引用されています。
これは楽しみですね。RubenMartinsさんも著者に入っています。 
インド工科大学については、こちらが詳しいです。https://diamond.jp/articles/-/91668

コンペティションのキックオフ直後に論文が、沢山出てくるのは、キックオフ前に公開してしまうと、
自分の優位性がなくなってしまう可能性があるためです。言い換えれば、前年の技術よりも優位な技術があるということです。しかしながら、次年度以降、誰でも、また、それを土台にして発展させることが可能です。その意味で、MaxSAT コンペティションは、重要な礎となってきましたし、SAT技術の発展に寄与してきたと思います。Communityのオープンな雰囲気は、文化と言ってもよいかもしれません。まだまだ、来年度以降も新しい可能性があると思います。

2018年6月17日日曜日

引用されています。

インテルのイスラエル ハイファ研究所のNadelさんの最新論文で去年出場したmaxrosterが引用されています。
http://www.cs.tau.ac.il/research/alexander.nadel/sat18_maxsat.pdf

全然関係ないですが、イスラエルのハイファというとCPUのコア2アーキテクチャの源になりますね。ハイファはイスラエルのハイテク産業の一大集約地になっています。

Nadelさんは、SAT SolverのCore Extractionという分野で有名な方です。 CPUに限らず、LSIのデザイン検証では、SAT SOLVERはなくてはならない重要なツールになっています。

光栄の至りです。


2018年6月12日火曜日

看護総会

今日(6月12日)、 マルマンコンピュータさんが出展されている、という情報を得ました。高速ソルバー(エンジン)が搭載されています。

是非、デモをご覧いただけたら、と思います。

実は、私も実物は、見たことはないのですが、院内LAN上、WEBブラウザで動くシステムです。基本的には大規模病院向けです。

2018年6月9日土曜日

Maxsat Evaluation 2018

昨日、どんな状況かなと思ってStarExecを覗いてみたら、ログインできませんでした。

その後、カーネギメロン大学Ruben Martinsさんから、丁寧なご招待を頂いたのですが、その返事を記しておきます。

Dear Ruben Martins-san,
Thank you for kind offer. Unfortunately, I can not submit the new version of maxroster this year due to heavy work for my real job. So, the website issue yesterday is not problem for me.

>and with your permission we can
>just reuse it for this year's evaluation.

No problem,You can reuse the maxroster for any purpose of evaluations in Maxsat Evaluation 2018.
I pray for Maxsat community making even great progress in 2018.
Best Regards,
Tak.Sugawara

>Dear Takayuki Sugawara,
>
>We had some technical issues with StarExec yesterday and the website was
>down for a few hours. We wanted to know if this affected you in any way
>since we noticed that you did not submit any solver to this year's
>evaluation.
>
>Since maxroster was the best solver for the incomplete track at the MaxSAT
>Evaluation 2017, we would like to know if you want to resubmit the same
>version to the MaxSAT Evaluation 2018. We still have the code, binary and
>description from last year's evaluation, and with your permission we can
>just reuse it for this year's evaluation.
>
>Alternatively, if you want to resubmit a new version of your solver, you
>can still do so until Monday, June 11.
>
>Best regards,

OR学会誌6月号

は量子コンピュータに関する特集です。ナーススケジューリングと関係ない? かもしれないし、もしかすると関係あるのかもしれません。 特集中、量子アニーリングによる組合せ最適化 というのがあります。実は、ナーススケジューリングは、組み合わせ最適化というOR分野の中のひとつにすぎません。その意味で、組み合わせ最適化が行えるのであれば、方法は問わないはずです。私自身、全くの門外漢で、上記特集記事により少しだけ雰囲気を見た程度です。それでも、去年のMaxSAT Evaluationsで、イジングモデルを使ってMaxSATソルバーを構成していた参加者がいたりしていて(確か性能は全く出ていなかったと思いますが) もしかしたら今後の進展により可能性があるのかな、程度の認識です。

量子アニーリングは、こちらの記事が分かりやすいようです。
http://blog.brainpad.co.jp/entry/2017/04/20/160000

2018年6月2日土曜日

商標査定 インテリナビ

インテリナビ 

という商標を出願していたのですが、ようやく査定になりました。10ヶ月かかりました。査定なので、未だ登録ではありません。 登録料を払ってようやく初めて登録になります。商標には、区分という概念があって(特許の請求項に似ています) 区分数で登録料が変わってきます。特許の場合は、毎年ですが、商標の場合は、10年です。(分割で5年も可能)  料金計算はこちら。http://www.jpo.go.jp/tetuzuki/ryoukin/shutugan.htm

実装を改善して、商標に恥じぬ機能にグレードアップしていく所存です。これには、現在開発中エンジンの計算機能も入れこむ予定です。

MaxSAT Evaluation 提出期限延期 

主催者のカーネギメロン大学 Ruben Martins さんから、延期の連絡がありました。といってもほとんど時間がないですね。Ruben Martinsさんは、OpenWBOというソルバーで、毎年出場されている若手のホープです。また、去年、トロント大学のFahiem Bacchusさんとメールでお話しさせて頂いたのですが、Fahiem Bacchusさんは、IPソルバとのHybridソルバを提案していてMaxSAT界の重鎮です。「東京に来たことがある」とおっしゃていました。

この方々は、主催者側ではありますが、毎年、参加されています。
今年は、去年の私を越えるソルバーが出てくるんでしょうか?多分参加してなくてもリファレンスにされるのでそれもまた楽しみです。下にもあるとおり、MaxSATベンチマークテストを提出すると皆でよってたかって解こうとしてくれるので、未解決問題を提出してみるのも一考に値するかと。

<MaxSAT形式の問題点>
去年やっていて気付いたのですが、問題のフォーマット形式がDIMACSというSAT問題を拡張した形式になっています。問題によっては意図が歪められてしまうということがあります。SAT形式ですので、どうしても2値化されてしまいます。オリジナルの問題が、整数計画であっても、無理やり2値化してしまうので、その辺がIPソルバーでは、つらいことになってしまうという面も否定できません。無論オリジナルの問題そのものが2値問題(例えば数独のような)であれば、なんの問題もないのですが。比較するべきは、オリジナル問題で比較するべきではないか?というちょっと主題からは外れたうがった見方をしてしまいます。ともあれ、ここ数年の成果は、確実にありますので、意味のあるCompetitionに違いはない、と断言できます。


MaxSAT Evaluation 2018 deadline extended to June 7

Dear all,
The deadline for submitting benchmarks and solvers for the MaxSAT Evaluation
 2018 is extended to Thursday June 7, 2018.
We encourage participants to test their solvers in StarExec in the testing
spaces:
- MSE2018->Testing->Complete->Unweighted
- MSE2018->Testing->Complete->Weighted
- MSE2018->Testing->Incomplete->Unweighted
- MSE2018->Testing->Incomplete->Weighted
The final version of your solver should be uploaded to the following
subspaces (depending on the category you want to participate):
- MSE2018->Evaluation->Complete->Unweighted
- MSE2018->Evaluation->Complete->Weighted
- MSE2018->Evaluation->Incomplete->Unweighted
- MSE2018->Evaluation->Incomplete->Weighted
More details on the final submission are available at:
https://maxsat-evaluations.github.io/2018/submission.html
So far we did not receive many new benchmarks. If you are using MaxSAT to
solve problems, we encourage you to submit your formulas to this year MaxSAT
 Evaluation.
New benchmarks are critical for the continuous improvement of MaxSAT solvers
and to perform a better assessment of their performance.
Best regards,

2018年5月31日木曜日

池上先生が全国紙に


http://mainichi.jp/articles/20180410/ddm/013/100/003000c

去年、研究室にお邪魔した際にも、学術分野に不慣れな私に、丁寧に意義を説明してくださいました。この分野の世界的権威であるにもかかわらず、飾らない実直な人柄で、ネットワークの図も見せて頂きました。最先端の一旦を垣間見ることができました。

2018年5月29日火曜日

新しい解の発見

ほとんどのインスタンスは、既に解かれてしまっています。

解のOptimumが未知のインスタンスは、あまりありません。狙い目は、解かれていないInstance15、そしてInstance19以上です。Instance19以上は、超巨大なインスタンスで、開発中のソルバーも、悪戦苦闘していますが、このレベルだと、現在、コンパイルすら通らない有様です。ところが、Instance15は、なんとかなりそうなのでやってみました。

今日現在、
http://www.schedulingbenchmarks.org/

のインスタンス15のKnownBestValueは、3834です。この値は、Pieter Smet さんが10時間回したBest値です。

数時間回したら、3831を発見してしまいました。この解は、多分、人類未踏の解です。ナーススケジューリングの歴史に名を残せそうです。

大規模インスタンスに対する改善を行って、他のインスタンスについても新しい解を得ることが6月の目標です。実は、このベンチマークのインスタンスは、実務から言うと特殊でして、このインスタンスセットについて、飛び切り優秀だとしても実務インスタンスの性能向上にはほとんど役にたちません。実務インスタンスに応用するには、もう一段手を加える必要があります。それが終了して、製品化実装を行って、初めて世にでることになります。発想から一年以上かかっています。



2018年5月20日日曜日

MIPソルバーの評価

例のベンチでの評価結果です。厳密解を得るまでの時間を
まとめてみました。(NEOSサーバによる)Instance8だけは、5分内に厳密界を得ることができず、最良値を書いています。
なお、自分のエンジン(ScNurse2)については、Pieter Smetさんの解を元に解析を進めてバグをFIXすることが出来、無事、厳密解1300を得ました。この解を得るまでに907秒かかりました。

なお、これ以上良い解はない、という証明には、さらに時間がかかります。MIPソルバーの方は、CuttingPlaneという数学的な方法で、LowerBoundを上げているので、解が見つかってから証明終了までさほど時間がかかりません。

RosterBoosterは、ノッティンガム大学のスピンオフ会社です。300sec以内に解けていないものが多いです。赤字で記したのがそのインスタンスでのBestSolverです。ScNurse2は、実装上の最適化チューニングを施していません。(未だ余力があります)


 CBCSCIPCplexGurobiRosterBoosterScNurse2ScNurse2備考
Instance11.81.670.150.2700.47 
Instance24.624.680.660.9800.5 
Instance3 30.33.11.621002(300sec)1.15 
Instance4 51.513.184.53101.11 
Instance5 235.0456.9134.39213.54 
Instance6  30.1514.71952(300sec)6.15 
Instance7  84.95113.541062(300sec)218.5 
Instance8(300sec)  166517941528(300sec)13011300(907sec)