完備化の問題をいくつか解いてみた

概要

先の記事に書きましたとおり、等式の完備化ツールをCommon Lispで作ってみています。

zkat.hatenablog.com

このツールを使って、いくつかの問題を実際に完備化してみたいと思いました。

試してみる

とは言っても、いい感じの入力となる問題を自分で作るのは難しいなと思っていたところ、以下を見つけました。

https://www.jaist.ac.jp/project/maxcomp/experiments/eq_systems.tar.gz

こちらは、JAISTの廣川研究室で開発されているツールMaxcomp（Maximal Completion）の 評価に用いられている問題のようです。

こちらの問題(合計115個)を利用させていただき、実行してみたところ以下の通りの結果となりました。

項目	値
実行環境(CPU)	Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz
実行環境(メモリ)	6GB
実行環境(OS)	Ubuntu 20.04.1 LTS on WSL2
完備化できた問題の数	65
完備化に失敗した問題の数	6
タイムアウトした問題の数	44
合計問題数	115

一つの問題ごとに、タイムアウトは30秒を設定しています。 だいたい、半分程度の問題を完備化するにとどまりました。

結果の詳細

Results of the Knuth-Bendix completion algorithm implemented in the tool Clover https://github.com/moratori/clover · GitHub

補足

以下のように実行しています。

$ wget https://github.com/moratori/clover/releases/download/v2.2.1/clover-linux-x86_64_ver2.2.1
$ chmod +x clover-linux-x86_64_ver2.2.1
$ time timeout -k 3 30 ./clover-linux-x86_64_ver2.2.1 complete slothrop_ackermann.trs
a(s(x),s(y))=>a(x,a(s(x),y))
a(s(x),Z)=>a(x,s(Z))
a(Z,x)=>s(x)

real    0m0.170s
user    0m0.227s
sys     0m0.042s
$