MiniSAT を mac で動かしたメモ #C++

はじめに

こんにちわ、ユニバの 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 の学習を始めましょう。