Category Archives: ECLiPse

[Debian]LinuxでECLiPSe CLPをビルドする

LinuxでECLiPSe CLPをビルドする手順を書きます。

何でビルドするかというと、先日ECLiPSeのメイン開発者の Joachim Schimpf さんに「ECLiPSeのContributorになりたい」というメールを送ったら、「ビルド・インストール関連の作業でできることがたくさんあり、例えばDebian packageなど出来ればよい(今は./RUNMEという独自シェルスクリプトでインストールする)」と言われたので、その作業の一環としてやってます。ビルドのやり方を記事にまとめるのも立派なContribute作業だと思いますので以下に手順記載します。

ちなみにただインストールするだけならばずっと簡単な手順があり、そのうち紹介します。

ディストリビューション:Debian バージョン10.9
ECLiPSe CLPのバージョン:7.0_54
目標:ダウンロードしたソースから、root以外の全ユーザーがtkeclipseコマンドでtkeclipse起動・eclipseコマンドでeclipse起動できる状態までもっていく
この作業でできないこと:
COIN-ORのインストール
CPLEXのインストール
XPRESS-MPのインストール
JAVAインターフェースのインストール
GraphVizのインストール
FlexLMのインストール
MySQLインターフェースのインストール

ディレクトリ構成やアーキテクチャ(以下の例では64bit)など、適宜自分の環境に読み替えてください。また、ソースをビルド・インストールする際はソースディレクトリのINSTALLファイルなど目を通しておいてください。

以下はDebianをインストールした直後からの手順です。基本rootで作業してます。

ECLiPSeダウンロードページ
/usr/local/srcに移動し、wgetでECLiPSeのソースを取得し、解凍する
0621_001

build essential をインストールする
0621_003

mkdir /vol/Eclipse/thirdparty を作成し、ECLiPSeのサーバからtcltk.tgzを取得・解凍する(最新の8.6のライブラリだとコンパイルエラーとなるのでここで手に入る8.5を使用します)
0621_004

0621_005

ディレクトリの名称をtcl8.5に変更します
0621_006

m4をインストールします(次のGMPのビルドで必要となる)
0621_008

GMPのソースを取得、解凍します。lzファイルの解凍のためにlzipインストールします。
0621_009

0621_010

gmpのフォルダに入り./configureを実行
0621_011

makeを実行
0621_012

make checkを実行
0621_013

make instalを実行
0621_014

はじめにダウンロードしたEclipseのソースのフォルダに移動します。
ECLIPSEARCH=x86_64_linux
ECLIPSETHIRDPARTY=/vol/Eclipse/thirdparty
を設定したのち、./configureを実行(詳しくは同じフォルダのINSTALLというファイル見てください)
0621_015

make -f Makefile.$ECLIPSEARCH を実行
0621_016

./RUNMEを実行
0621_017

Enter押下
0621_018

Enter押下
0621_019

インストール先は/usr/local/binにしました。
0621_020

Enter
0621_021

tcl/tk用のパス設定を行います。多分このままで良いのですが、一応配置した/vol/Eclipse/thirdpartyに変更しました。
0621_022

0621_023

0621_024

不要となった圧縮ファイルを削除します。
0621_025

exitで一般ユーザーに戻り「tkeclipse」コマンドでtkeclipseが、「eclipse」コマンドでeclipseが起動するようになりました。
0621_026

0621_027

ECLiPSe の Nonogram Solver の解説

ECLiPSe CLPのexampleページにあるnonogram solverを解析していて、大体理解したので説明します。(内部で regular expression constraintを使用しています。)
nonogramは日本でいうところのお絵かきロジック、ピクロスです。

ルールの説明は割愛します。

プログラムの説明も細かいところ端折ってエッセンスの説明だけします。
このプログラムの一番重要な部分は、それぞれの行列のヒントのリスト(例えば[3,3,2]など)から盤面を表すリストの制約を生成するline述語で、この内容がわかれば8割方理解したことになります。

line述語にはヒントのリストと盤面1行分(or1列分)のリストを渡します。
line述語内でfromtoを駆使してヒントからTableに怪しげなリストを生成しています。

以下の例では、tkeclipseのコンソール?で
length(Xs,15),line([3,2,3],Xs).
と入力してステップ実行した結果です。これは、ピクロスの問題でいうところの、ヒントとして「3,2,3」が与えられた15マスの1つの行の制約をつける処理に相当します。

このfromtoの説明も今回は割愛します。このプログラムではあまり良い使い方してないので他の例で学んだほうが良いです。fromtoなどのLogical Loopはかなり重要なのでいつか改めて解説記事書くと思います。

このTableなのですが、fromtoの操作が終了した時点では図のような内容になっています(右の四角内)
nono

並べ替えて書くと以下の内容です(ここら辺ぐちゃぐちゃに登録してるのがこのプログラムの良くない≒テキトーなところなので見習わなくて良いです)
[0,1,1]
[1,1,2]
[1,2,3]
[1,3,4]
[0,4,5]
[0,5,5]
[1,5,6]
[1,6,7]
[0,7,8]
[0,8,8]
[1,8,9]
[1,9,10]
[1,10,11]
[0,11,11]

このリストなのですが、オートマトンの状態遷移表を意味していて、盤面のリストを左から読み込んでいった際の状態の変遷を記述してます。
3つある数字の意味は
[読み込んだ数字(0 or 1), 現在の状態, 次の状態]
を表していて、
「現在の状態 で 0または1 を読み込んだら 次はどの状態になるか」
をすべて書き出しています。

状態を11個持つ以下のようなオートマトンが出来たことになります。便宜的に状態にqをつけました。
automaton

状態はq1から開始し、矢印に書いてある数字を読み込んだ際に次の状態に遷移します。
矢印がない数字が入力された際はヒントの条件を破ってしまっているのでオートマトン不受理(エラー、制約違反)となります。
q11の状態が最終状態(受理≒読み込み終わったときにこの状態であればOK)となります。

状態遷移表が完成したのち、それをregularという術語に渡して実際の制約を作成しています。

regularの説明です。
Qsは状態のリストです。この例では15個数字を読み込むので、それぞれの読み込み時に対応したものとなります。作成したオートマトンから、上記の例だと最初の状態がq1、最後Qnがq11となります。
与えられた盤面の1行(列)のリストに「現在の状態」「次の状態」の2つの変数を追加して
[マス目の数字, 現在の状態, 次の状態]
が1要素となるリスト(この例だと要素は15個)を作成しています。
状態の部分にはQsの要素を順番に指定して以下のように隣の要素同士を関連付けています。
nono_juzu

そして、それぞれの要素に関し
(Goal infers ac)@Module

で実際の制約をつけるのですが、これが実際どのようにコールされているかというと、
member([マス目の数字, 現在の状態, 次の状態], List) infers ac
という呼ばれ方です。Listの中身はオートマトンの状態遷移表です。
この操作で、[マス目の数字, 現在の状態, 次の状態]の3つの組が、オートマトンの状態遷移表の要素のいずれかの組み合わせに一致する(それ以外の組はありえない)という制約を設定しています。

member(A,L)はご存知の通り「AはL内の要素の一つ」を表すprologの組み込み述語で、ECLiPSeの制約ではありません。
ここで使用されている 「infers」というのがこのブログでも何度か触れたpropiaという仕組みで、任意のprologの述語(組み込み述語でも自作述語でも良い)をECLiPSeの制約に変換してしまうというすごい強力な仕組みです。memberは本来バックトラックを発生させてしまうため制約としては使用できないのですが、propiaを使用することにより「AはL内の要素」という意味の制約として機能するようになります。
infers ac の acの部分は制約伝搬の際にどの程度絞り込むか(候補の枝狩り)の動作に関連します。
acはarc consistency の略でアーク整合のことで、これは制約プログラミングの用語です。自分はぼんやりとしか把握してないのですがそのうちちゃんと理解したら記事書こうと思います。
infersのマニュアルページ

ちなみにECLiPSeは主にアーク整合アルゴリズムAC-3AC-5を使用しているらしいです。

制約を作るときにオートマトンを使用するというのは面白いアイデアで今後何らかの参考になるかもしれません。

Nonogram Solverは今回解説したオートマトン使用したものの他にECLiPSeメイン開発者のJoachim Schimpfさんが作成したgecodeバージョンがあり、こちらのほうが記述が簡潔なのでそのうち解析してみたいです。

Project Euler 46

久しぶりに解きました。
あんまり良いプログラムではないけど…

Problem 46(日本語)
Problem 46(本家サイト)


実行結果(回答伏せます)
solve.
answer XXXX = XXXX * XXXX
Aborting execution ...

CHRをGPUで実行させる論文を読みました。

Parallel Execution of Constraint Handling Rules on a Graphical Processing Unit
という論文を読みました。
リンク
リンク切れている場合は論文名で検索してください。

Constraint Handling Rulesの開発者のThom Fr¨uhwirth さん達が書いた論文で、CHRをGPU上で実行させる方法がCUDAのコード込みで書いてあります。

Constraint Handling Rulesに関して自分がわかっているレベル(≒あまりわかっていない)で簡単に説明すると、CHRは基本的には記述された一連の制約を論理的に同等かつよりシンプルなものにしたり、何かに変換(自作の制約で書いた記述 → 組み込み述語のみ使用した記述に変換など)したりします。

例えばECLiPSeではPropiaとは別にCHRを使用しても自作の制約が定義出来ます。

まず以下の3種類のいずれかの構文でルールを記述しておきます。(これが自作制約となります)
CHRには以下の3つしかルールがありません。
・simplification
  Head1,Head2 <=> Guard | Body
・propagation
  Head1,Head2 => Guard | Body
・simpagation
  Head1¥Head2 <=> Guard | Body
(HeadもGuardもBodyも普通のPrologのCallable Termで書きます。
GuardとBodyの部分は複数の述語を書いて良い。Headの部分は最大2つの述語のみ(ECLiPSeの場合。3つ以上が不可なのは以下に述べる述語のピックアップの際の効率の問題らしいです)→すみません訂正します。CHRの昔のライブラリでは2つのみでしたが、新しいECHライブラリでは3つ以上可能でした)

動作の仕組みなのですが、上記で定義した制約を含む述語群を連言(=AND。カンマ区切りの普通のPrologの表現)で記述すると、CHRの機構はそれらの述語群の中から2つピックアップし、
・上記のHead1,Head2にパターンマッチ
・GuardがTrueとなる
を満たすものを見つけると、以下のルールに従ってピックアップした2つの述語を「書き替えて」しまいます(これをfire[発火]と呼ぶ)そしてその際にBodyの実行可能な述語は実行してしまいます。
また、Guardの部分は常時チェックされる番犬のような動作をしていて、例えばguardにnonvar(A)みたいな記述をしていた際、別の処理でAに何か値を設定した場合、その瞬間にGuardのチェックが通り対応するBodyが発火されます(ECLiPSeのsuspend機構を使って実装されている)
simplificationの場合はBodyに書き換え
propagationの場合はHead1,Head2そのままでBodyの述語を追加
simpagationはHead2のみBodyに書き換え(Head1は残す)

上記の変換を適用できるルールがなくなるまで繰り返す(2つ述語ピックアップ→Head1,Head2にマッチングするかチェック→GuardがTrueかチェック→ルールに従いHead1,Head2を書き換え)
どうも書き換え中のルール群をconstraint storeと呼んでいるようです。

ちなみに上記一連の処理中にはバックトラックは発生しません。
CHRの動作を「コミッテドチョイス」と言うらしいのですが、CHRの機構がどの述語をピックアップするか勝手に決めるのでプログラマはコントロールできない(選択を委託する)という意味かもしれません。
また、Headの部分は2つじゃなくて1つでも良いです。

CHRは基本的には上記の書き換えを行うのみなので、用途は特に制約の表現のみにとどまらず、サンプルを見ると
 最大公約数の計算
 ガウスの消去法
 高速フーリエ変換
 マージソート
など、色々な応用があります。

めちゃめちゃ端折ってますが上記がCHRの基本動作です。

記述した制約群をどのような組み合わせでピックアップ・変換したとしても必ず最終的に生成される述語群が同じになるようなとき、Confluence(合流)性を持つと言うそうです。

Confluence性はどのようにすれば担保されるかなのですが、以下の論文に書いてありますが自分はまだ理解できていない(論理学の用語がたくさん使用されてて難しいため)どうも冗長なルールを追加することにより合流性が担保されるようです。

Theory and practice of constraint handling rules
リンク切れしている場合は論文名で検索してください。

Confluence性を満たす場合CHRが並列処理に非常に向いているとのことで、理屈では確かにそうだなと自分も納得しました。

前置きが長くなりましたが、上記を踏まえたうえでGPUでCHRを使った上記の論文を読んだわけです(GPUは数千コア積んでいるものもあり単純な計算を同時に行うのに非常に有力)
論文の内容はCUDAコードが実際に記載されていて実装イメージがしやすいものでした。
しかし、ルールの述語自体をCUDAコンパイル用のコードで書いているため、あまり汎用性がないのではないという気がしました。
使う側は当然任意の述語を使いたいのですが、論文のやり方ではそのたびに新たなプログラムをCUDA用に書いてコンパイルしなくてはならないのでは?と感じました。
あまりGPUのことわかってないですが、if文を多用するプログラムは遅くなるなど、性能を100%出すためにいろいろ条件があるようです。
現状ではCHRをGPUの速度を100%出し切って実行するのは難しいのかな、と感じました。
ただ理論的にCHRのいろいろな性質が証明されているので、ハードウェア側でCHRに向いた実装が実現されたら、かなり望みがあるような気がします。

余談ですが「CHRには3つしかルールがない」と書きましたが、
・simpagation
  Head1¥Head2 <=> Guard | Body
の、
・simplification はこれの Head1 がないバージョン(Head2がBodyに書き換えられる)
・propagation はこれの Head2 がないバージョン(Head1そのままでBodyが追加される)
となるので実質はsimpagationだけで良いみたいな文章をどこかで読みました。

labelingに関して

制約論理プログラミングで必ず出てくるlabelingに関して説明しようと思います。
だだーっとマニュアル見ないでいい加減に書くので多分嘘も書いてますが大体で読んでください。なるべくプログラム自体も書かない記述にします(めんどくさいので)

概要的にはECLiPSe CLP のtutorialに書いてあることを抜粋して書くので英語読める人はそちらを読んでもらう方が絶対に良いです。とても分かりやすいです。
ECLiPSeのtutorial

制約論理プログラミングでは基本的なプログラムの構造は以下のような形になってます。
1.制約の記述
2.解のサーチ
3.解の表示

labelingというのはこれの2.解のサーチに相当します。

labeling述語には制約変数のリストを渡します。
例えば、(便宜的に整数のみ扱います。というか整数しか自分は扱い方が良くわかりません。)
変数Aが1から3
変数Bが1から3
変数Cが1から3
といった制約をつけた後、labeling([A,B,C])というような呼び出しをすると、A=1,B=1,C=1という解が設定されます。
Prologをやっている人はピンとくると思いますが、labelingの呼び出しでバックトラックが発生し、failすると次のA=1,B=1,C=2という別解が設定されます。バックトラックするごとに制約を満たす解が順番に設定されます。

ちょっと余談で、ECLiPSe CLPの資料を読んでるとことあるごとに口酸っぱく書いてあるのですが
「1.の制約の記述の部分は、バックトラックを発生させてはいけない」とのことです。制約の部分でバックトラックを発生させる作りにすると正確な解が得られないとのことです。
バックトラックの有無がPrologの一般的な述語と制約論理プログラミングの制約の大きな違いだと思います。
ですので、ECLiPSe CLPにもSWI-PrologのCLPFDにもたくさん制約用の述語が定義されてますが、そのどれもがバックトラックをしない述語になってるはずです。

これもまた余談ですがECLiPSeには自分が任意に定義したPrologの述語を制約に変換することが出来るPropiaという仕組みがあり、とても便利です。これを使うとバックトラックを生成させてしまう術語がバックトラックを生成しない制約に変わります。

話は戻って、labelingなのですが、既定では与えられた変数群の解を生成する際、
・リストの先頭の変数から順番に値を確定
・値はドメイン(取りうる範囲)の小さいほうから大きいほうへ
決定しています。

ただ、これが一番良いやり方かどうかはわかりません。
SWI-PrologのclpfdでもECLiPSe CLPでも「どの変数の値を優先的に決定するか」「値をどのように設定するか」の2つの観点でいろいろなオプションが用意されてます。
例えば以下の観点のオプションなどあります。
・一番ドメインの範囲(取りうる値の範囲)が小さい変数から決定する
・値を中央から外側に向かうように設定する
・値をランダムに設定する

SWI-PrologのCLPFDではここまでの話でlabelingに関しての説明は完了なのですが、ECLiPSe CLPはこのlabelingの部分を完全にプログラム制御できます。tutorialのTree Search Methodの項を見てください。

まずlabelingを使用せずに、1つの制約変数を指定して、
indomain(変数)という書き方ができます。
これは変数の取りうる値を小さいほうから順に設定してfailするたびバックトラックをさせるという、labelingの1変数バージョンのような述語です。そしてindomainの2番目の引数にオプションを渡すと、いろいろな順番で値を決めることが出来ます(大きい順、ランダム、真ん中から、etc…)

また、deleteという紛らわしい名前の述語があるのですが、これにfirst_failなどのオプションを指定して制約変数のリストを渡すと、指定したオプションに応じたやり方で1つ変数を取り出し、それ以外の変数をRestに返してくれます。
first_failの場合はリスト内の一番ドメインが少ない変数を選択し、残りをRestで返します。
(「次に値を決める変数の選択」を行ってくれる述語)

ECLiPSeではこのdeleteとindomainを駆使して、細やかに変数のラベリングをコントロールできます。ECLiPSeのtutorialには、これらを使用してN-Queenの問題をいろいろなラベリング方法で解き、かかった時間を計測するという興味深い記事が出てますので是非読んでみてください。

あとsearch/6という似たようなことする術語もあるのですがまだよくわかってません。
あとECLiPSeでは整数以外の値が扱えるのですが、そのときにindomainの実数バージョンのようなlocateという術語があるのですが、これもまだ詳細に使いこなせてません。

これ読んでる方もぜひ一緒に勉強しましょう(そして教えて下さい)

DOMINO PUZZLEソルバーの解説

ここ最近、勉強で ECLiPSe CLPのExampleページのドミノタイル問題ソルバーのソースを解析していました。大体理解したので解説したいと思います。

問題の解説:
0-0、0-1、0-2…..6-6 の全部で28枚のドミノタイルがある。
tiles

このタイルが横8×縦7の長方形の中にランダムに敷き詰められている。
縦、横、左右逆、上下逆のどの置き方でも良い。

どのように置いたかは不明で、並べた結果全体の数字が以下のようになっていた場合、タイルがどのように配置されていたかを解け。
3 1 2 6 6 1 2 2
3 4 1 5 3 0 3 6
5 6 6 1 2 4 5 0
5 6 4 1 3 3 0 0
6 1 0 6 3 2 4 0
4 1 5 2 4 3 5 5
4 1 0 2 4 5 2 0

プログラムの解説:

プログラムの概要を説明します。
①述語one_by_two_tiling/4でLeftとUpというマス同士の接続状態を表す配列を作成、制約を設定します。

Leftの配列は以下の色のついた部分の接続状態を表す2次元配列です。
1つのドミノタイルとしてつながっていれば1、つながっていなければ0になります。
lefts

Upは以下の色のついた部分の接続状態を表す2次元配列です。
Ups

制約のつけ方なのですが、あるマスに注目し上下左右の接続状態を考えたとき、必ず上下左右のいずれか1つの方向のみ接続されていることになるので、そのような制約を設定します(上下左右の変数の和が1)

②2つのdo文で、隣接した2マスに注目しながら、「2つの数字-対応する接続変数」の組み合わせをどんどんリストに集めます。このとき、タイルは数字が小-大の順番になるようにして保存します。
その部分にタイルが配置されていた場合は、該当する接続状態の変数が1になるというわけです。

scan
ヨコ方向の隣接マスに注目した後は、タテ方向で同様の操作を行います。どちらも同じ配列にまとめます。
このようにまとめると当然 (1,4)-変数 というような組み合わせが複数見つかりますが、いくつか見つかった中のどれか1つの組み合わせだけが実際に配置されているタイルの情報だということになります。

③まとめた配列をkeysortでソートします。タイルごとにまとまります。

④group_same_key_values/2で、ソート後の
[...(1,4)-接続状態変数1,(1,4)-接続状態変数2,(1,4)-接続状態変数3,(1,5)-接続状態変数4,(1,5)-接続状態変数5...]
のような状態のリストを
[…(1,4)-[接続状態変数1,接続状態変数2,接続状態変数3],(1,5)-[接続状態変数4,接続状態変数5]…]
のような形式にまとめます。


[接続状態変数1,接続状態変数2,接続状態変数3] の和が1
[接続状態変数4,接続状態変数5] の和が1
というような制約を設定します(foreach)

⑥term_variableで全変数を1つのリストにまとめた後labelingですべての接続状態変数の解を探します。


prety_print出力結果:
pretty_print

Project Euler Problem 62

Problem 62

ECLiPSe CLP で解きました。
ほぼPure Prolog で、制約論理の述語は使用してません。
自分のマシンで約9秒。

プログラム:

コマンドライン:

?- time(go).
Yes (9.22s cpu)

標準出力:

<解答伏せます。>

Success, times: 9.218750s thread, 9.219+0.000s process, 9.224s real

Project Euler Problem 59

Problem 59

全体の文字数 – 「何文字がA-Z a-zの範囲だったか」 の数値をコストとして計算し、一番コストが小さくなるものをbb_minで調べました。
あんまり効率よくないプログラムで、1900秒くらいかかりました…遅いな…
あとテキストの文字数が3の倍数というところは前もって調べてて、それをあてにしたプログラムになってます(文字数が3の倍数でないとdecryptでこける)

ソース

実行結果

Project Euler Problem 52

Problem52

ECLiPSeで解きました。
処理時間は自分のマシン(Intel(R) Core(TM) i5-3340M CPU @ 270GHz)で6.5秒くらい。
見どころ?はECLiPSeのlogical-loopで書いた順列permutationと、propiaで数値を入れ替えた制約を作っているところ
logical loop はループ用のサブ述語みたいなアホっぽい定義がなくなってコードがエレガントになるのでSWI-Prologでもぜひ正式採用してほしい。
桁のところは一般化してなく、1桁、2桁、3桁… と手入力で増やしながら確認しました
(bb_minでそれぞれの桁での最小の数値が取れるようにしてます)。

プログラム:

実行結果(解答伏せます):

[Prolog] DCGで双方向性のある述語を作成

最近stackoverflowでPrologの質問に良く回答しているのですが、面白そうな問題があり、自分でもプログラムを作ってみました。

質問

内容は、[1,2,3,4,1,4,7,5,7,8,9] のようなリストが与えられた際に「続いている数字は[最初の数字,最後の数字]の形で表し、そうでないものは単体の数字で表したようなリストを生成する という問題です。
[1,2,3,4,1,4,7,5,7,8,9]は[[1,4],1,4,7,5,[7,9]] に変換されます。

作っているうちにどんどんアイデアがわいてきて、はじめは長いプログラムだったのがDCG使ってエレガントな方法で実装する方法を思いつき、最後には入出力逆転してもOKなような非常に汎用的な形で作成できました。

ECLiPSeで作成(多分他の環境でも問題なく動きます):

実行結果:

最後のマッチング例は「やってみたら、できた」という実験で、自分の予想を上回る汎用性が実現できていてびっくりしました。

入出力がどちらもリストの述語を作成するときは、工夫すると双方向性が実現できることがあると思います。

Prologの真髄に触れたような気がしました。