🍬

制約ソルバSugarのインストールメモ(Ubuntu)

に公開
sugar
tech

Sugar: a SAT-based Constraint Solver 2.3.4 をUbuntu 18.04にインストールした際のメモ

依存パッケージのインストール

sudo apt install minisat default-jdk

インストールスクリプト

/usr/local 以外にインストールしたい場合は以下のようにパッチを当てる必要がある。

#!/bin/sh
set -eux
prefix="$HOME/.local"
mkdir -p sugar
cd sugar
git clone https://gitlab.com/cspsat/prog-sugar.git
cd prog-sugar/
patch -Np1 << EOF
diff --git a/Makefile b/Makefile
index 50462c7..341b157 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,8 @@
 VERSION = 2.3.4
 
 APP0 = sugar
-BINDIR = /usr/local/bin
-LIBDIR = /usr/local/lib/\$(APP0)
+BINDIR = $prefix/bin
+LIBDIR = $prefix/lib/\$(APP0)
 
 APP = \$(APP0)-\$(VERSION)
 JAR = ./build/\$(APP).jar
diff --git a/sugar b/sugar
index 52e0490..58d1a0c 100755
--- a/sugar
+++ b/sugar
@@ -12,7 +12,7 @@ \$| = 1;
 
 my \$version = "2.3.4";
 my \$java = "java";
-my \$jar = "/usr/local/lib/sugar/sugar-\$version.jar";
+my \$jar = "$prefix/lib/sugar/sugar-\$version.jar";
 my \$solver0 = "glucose";
 my \$solver0_inc = "minisat-inc";
 my \$tmp = "/tmp/sugar\$\$";
EOF
make all install

動作確認

$ sugar -v -solver minisat /path/to/prog-sugar/examples/nqueens-8.csp
c 0	Sugar 2.3.4 + minisat
c 0	BEGIN Sun Aug 21 19:24:18 2022
c 0	ENCODING prog-sugar/examples/nqueens-8.csp TO /tmp/sugar24673.cnf
c 0	ENCODING CPU 0.34 (0.01 0 0.3 0.03)
c 0	SOLVING /tmp/sugar24673.cnf WITH /tmp/sugar24673.map
c 0	SAT SOLVING /tmp/sugar24673.cnf
c 0	DECODING /tmp/sugar24673.out WITH /tmp/sugar24673.map
s SATISFIABLE
a q_1	7
a q_2	2
a q_3	4
a q_4	1
a q_5	8
a q_6	5
a q_7	3
a q_8	6
a
c 0	DECODING CPU 0.13 (0 0 0.11 0.02)
c 0	SOLVING CPU 0.14 (0 0 0.12 0.02)
c 0	CPU 0.49 (0.02 0 0.42 0.05)
c 0	END Sun Aug 21 19:24:18 2022

おまけ

何となくDockerfileを作ってみた

FROM ubuntu:22.04
RUN apt-get update \
    && apt-get install -y --no-install-recommends minisat default-jre curl make \
    && apt-get clean \
    && rm -rf /var/lib/apt/lists/* \
    && curl https://gitlab.com/cspsat/prog-sugar/-/archive/v2.3.4/prog-sugar-v2.3.4.tar.gz | tar zx \
    && make -C prog-sugar-v2.3.4 install \
    && sugar -vv -solver minisat prog-sugar-v2.3.4/examples/nqueens-8.csp

Discussion