はじめに
こんにちわ、ユニバの MJ です。
普段はフロントエンドをしているんですが、社内の動きもありそろそろ C++ に手を出したいと思っていた時の話です。
SAT と SAT solver
この話はカナーーーーリ長くなるので割愛。でもここら辺を読んでくれれば嬉しい。
かくいう私も山がいっぱいある中の大学でSATを学んでいた一人です。
SAT というのは充足可能性問題のことで、それを解くのが SAT Solver です。
SAT は NP完全な問題として知られています。つまり数ある NP な問題でもっとも難しく解き方によっては指数的に時間がかかってしまう問題(こんな言い方であっているのかとても不安！)
ともあれ、Solver は この問題を効率良く解くための施策がいくつもされていて、それがとっても C++ の勉強に役立つ。ということです。
MiniSAT はオープンソース なので自分で改造して性能を伸ばすことができます。
ちなみに Solver の評価尺度はより早く問題を解くことなので、とてもシンプル。
コンペティションもあるのでみんなもやってみよう！
MAC で動かしてみよう
さて、上の話についてけた人なら当然
xcode は入っているだろうし brew も入っているでしょう。
入ってない人はとりあえず、入れましょう。
gcc
さて xcode 経由で入れた gcc のバーションは少し古いです(私は 4.2でした。)
これだと 最新の minisat-2.2.0 をコンパイルしようとすると error します。
/core/SolverTypes.h:50:16: error: friend
declaration specifying a default argument must be a definition
friend Lit mkLit(Var var, bool sign = false);
mkLit 関係で error しているようです。 これを解消するために gcc5系 を brew 経由で install しましょう。
brew install
まずは search
brew search gcc
そうすると次のような結果が返ってきました
gcc ✔
homebrew/dupes/apple-gcc42 homebrew/versions/gcc45 homebrew/versions/gcc48 homebrew/versions/gcc6
homebrew/versions/gcc43 homebrew/versions/gcc46 homebrew/versions/gcc49 homebrew/versions/llvm-gcc28
homebrew/versions/gcc44 homebrew/versions/gcc47 homebrew/versions/gcc5 Caskroom/cask/gcc-arm-embedded
どうやら私は brew install gcc していた模様。もしかしたら homebrew/versions/gcc5 しても良いかもしれない。
install した gcc を使う
install した gcc を見に行きましょう。私は brew で install したものは /usr/local/bin/ に入っているので確認します。
そうすると
gcc-5
g++-5
はい、version5 系の gcc が入っていました。
これを minisat のコンパイルの時に使うよう指定してあげましょう。
ちなみに コードは ココからダウンロードして
適当なフォルダに展開します。
そのあとで、展開したフォルダにこんな感じのシェルを書いておくと楽かも
# !/bin/sh
export MROOT=$(pwd)
cd ./core
make r CXX=g++-5
加えて、Apple 用に /utils/System.cc を次のように変更します。
# elif defined(__APPLE__)
# include <malloc/malloc.h>
double Minisat::memUsed(void) {
malloc_statistics_t t;
malloc_zone_statistics(NULL, &t);
return (double)t.max_size_in_use / (1024*1024); }
double Minisat::memUsedPeak(void) {return memUsed(); } <- この行を追記
# else
./build.sh を実行すれば gcc5系でコンパイルされ、solver の実行ファイルができるはずです。
終わりに
これを xcode で build して動かしたい気持ちになっている。できるかな。
とりあえずは terminal で動かして SAT の学習を始めましょう。