新しい解の発見 その2

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

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

	So Far Bestknown		New Solution
	LB	UB	LB	UB
Instance15	3823	3834	3824	3831
Instance20	4743	4943	4769	4778

116Aをリリースしました

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

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

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

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

マルチスレッド化検討

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

インテルの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

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

過誤納のお知らせ

ｘｘｘ様

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

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

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

特許証を受領しました。

いつもながら、書留ではなく普通郵便です。

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の方々に頭が下がる思いです。