Sugar制約ソルバーSugar: a SAT-based Constraint Solverは、パズルをSugar制約ソルバーで解くみたいな感じでパズルをSATのデータに変換してSATソルバーに丸投げして解かせる感じのソフトウェアです。たぶん動作環境としてはLinuxしか想定していなくてCygwin（Windows）で動かしたらハマったのでその対処法です。だいぶ昔にやったのを思い出して記事にしたので、もう今はWSLを使えばいいのかもしれませんが…。
1.Cygwinを導入する
パッケージをあとから入れるとautorebaseでめっちゃ時間がかかったりするらしい（僕は、ちょっと時間がかかりました） アンチウイルスを切ると治ることもあるらしい
（最新のminisatをビルドするなら、g++とmakeを入れておく）
（Sugarに必要なのでperlも入れる（もともと入ってる？））
2.Sugarを入れる
前述の公式サイトからダウンロードする。2.3.4からダウンロード方法が変わっており、以前のzipファイルと同じものはbuild · master · cspsat / prog-sugar · GitLabにある。jarファイルが本体で、sugarというperlスクリプト（以下、スクリプトと呼ぶ）が前処理・後処理をやっている。通常はこのスクリプトのほうを使えばいいはず。
なお、2.3.3まではJRE 8でも動いていたが2.3.4だとencodeに関するエラー
ERROR Exception java.nio.ByteBuffer.flip()Ljava/nio/ByteBuffer;
が出た。最新版のJDK（ver15）を入れたら治った。
3.(minisatをビルドする)
MiniSat Pageここからダウンロードできる。最新版じゃなくてよければMiniSat_v1.14_cygwinをダウンロードし、この節を読み飛ばしてよい。ビルドする気があるなら、minisat-2.2.0.tar.gzをダウンロードする。
READMEを参考にしながらビルドする。基本的には
cd core
export MROOT=..
make r
でいける。ただ、friend関数がなんとかみたいなエラーが出るので、言われた通り（？）コンパイルオプションに-fpermissiveを追加する。すなわちmtl/template.mkをいじって
CFLAGS ?= -Wall -Wno-parentheses -fpermissive
と変更する。するとうまくいきそうになるがこんどはldでmemUsedPeak()が見つからないというようなことを言われるのでutils/System.ccの最後の#endifの直前に
double Minisat::memUsedPeak() { return 0; }
という行を入れる。これで通るはず。なお上記2か所については調べたらすでにgithubにissueが投稿されていてプルリクエストもマージされているようだったがそちらをビルドしたらまたエラーが出たのでやめた（正式リリースされてないので当然か）。
なお、READMEに書いてある通りにmake rではなくmake rsとすると、static（といってもcygwin1.dllはないと動かない）なものができる。cygwin上で使うならmake rでいいはず。
minisatじゃなくて他のを使ってもいいと思う。スクリプトの中を見ると、minisatとかglucoseとかlingelingとかいくつか書いてあるので少なくともそれらには対応していることがわかる。lingelingも以前やってみたことがある気がするが忘れた。
4.スクリプトをいじる
このままsugarを実行するとno SAT fileと出てくる。これをどうにかする必要がある。
まずデバッグのためにsugarの実行時に-vvというvery verboseな出力を出してくれるオプションを付けると（例: bin/sugar examples/nqueens-8.csp -vv）、java.lang.ClassNotFoundExceptionが出ていることがわかる。しかし文字化けしていて不便なので、スクリプトの最初のほうの
を
my $java = "java -Duser.language=ja -Dfile.encoding=UTF-8";
に変えると、文字化けがなくなる（やはり"エラー: メイン・クラスjp.kobe_u.sugar.SugarMainを検出およびロードできませんでした"と出ている）。
要するにjava.exeがjarファイルを見つけられないということなので、さっきの次の行にある
my $jar = "/usr/local/lib/sugar/sugar-$version.jar";
の通り、cygwinのインストールディレクトリの中の/usr/local/lib/sugar/にjarファイルを入れる。
あるいは、最初のほう（useがいくつかあるところ）に
use FindBin;
と書いてから
my $jar = "$FindBin::Bin/sugar-$version.jar";
としてもよい。FindBinは、スクリプトファイル自体がある場所を教えてくれるやつで、sugarをダウンロードした状態のままならbinフォルダの中にスクリプトといっしょにjarも入ってるのでこれで動く。
ただ、Cygwinと（Windows上の）Javaの相性の問題で、このままではまだ動かない。スクリプトでjavaが関わる場所を見ると
sub java {
が見つかる。まず、この中身の6行目くらいにある
$cmd .= " -cp '$jar' $class";
を、
$cmd .= " -cp `cygpath -w $jar` $class";
に変更する（シングルクォート ' ではなくバッククォート ` になっていることに注意）。これだけでもさっきと結果が変わっているはず。cygpathはcygwin用のパスをWindows用に変換したりその逆をしたりしてくれるコマンド。これによりjava.exeがjarを見つけられるようになる。ためしに実行してみると
ERROR Exception \tmp\sugarXXXX.cnf (指定されたパスが見つかりません。)
などと出ている。これもjavaが入出力用のファイルを見つけられていないからである。そこで、sub javaに渡されている$argsの中身を直さなければならない。javaを呼び出している箇所を（&javaで検索して）調べるとconvertとtranslateとencodeとdecodeの四か所ある。なので、それぞれの中で$argにファイル名を格納している場所を同様に変更すればよい。通常の用途ならencodeとdecodeだけ変更すればよいはず。すなわちencodeについては、sub encodeの中の
$arg .= " -encode '$csp_file' '$sat_file' '$map_file'";
を
$arg .= " -encode `cygpath -w $csp_file` `cygpath -w $sat_file` `cygpath -w $map_file`";
と変更し、decodeについてはsub decodeの中の
$arg .= " -decode '$out_file' '$map_file'";
を
$arg .= " -decode `cygpath -w $out_file` `cygpath -w $map_file`";
と変更する。
そうすると今出てるエラーはsatソルバー（最初のほうのmy $solver0 = "xxx";に書いてあるもの）が見つからないというものになっているはず。そこで3.で得たminisatの実行ファイルをminisat.exeという名前に変えてcygwinのusr/local/binとかに入れ、
my $solver0 = "minisat";
に変える。あるいは先ほどのようにスクリプトと同じフォルダにminisatを入れて
my $solver0 = "$FindBin::Bin/minisat";
としてもよい。これで動くはず。動かなかったらコメントとかで教えてください。
なお、パスの変換とかをしてる関係で、入出力に関連するファイル・フォルダに半角スペースが入っていると動かない可能性が高いので注意。
