gophersat
1.0.0
これは、純粋に Go で書かれた SAT および擬似ブール ソルバーである Gophersat です。 Gophersat は、アルトワ大学と CNRS の CRIL (Centre de Recherche en Informatique de Lens) によって開発されました。 MITライセンスに基づいてリリースされています。 Gophersat はかなり効率的です。つまり、一般的な SAT ベンチマークでは、その元となったトップレベルのソルバー (つまり、グルコースまたはミニサット) よりも約 2 ～ 5 倍遅く実行されます。 MAXSAT 問題、擬似ブール決定および最適化問題も解決できます。
Gophersat の最後の安定バージョンはバージョン 1.4 です。これには、オプションの切断面解決戦略が含まれています。
有名な鳩の巣問題など、一部の問題は、純粋な論理的推論を使用して解決するには非常に長い時間がかかります。
鳩穴問題は次のように表現できます。数羽の鳩を同じ穴に入れてすべての鳩を 1 つの穴に入れることなく、m 個の鳩穴に n 羽の鳩を入れることは可能ですか (m = n-1)。答えは明らかです。3 つの穴に 4 羽のハトがいる場合、すべてを別の穴に入れることはできません。しかし、これをどうやって証明するのでしょうか？ SAT または PB ソルバーは、考えられるすべての組み合わせを試してそれを証明しますが、考えられる組み合わせの数は指数関数的に増加します。したがって、問題には明白な答えがあるにもかかわらず、n=20 で問題を解決しようとすることは実際には不可能です。
一部の PB ソルバーは、代替戦略である切断面戦略を実装しています。この文書では詳しく説明しませんが、この戦略は、純粋な論理的推論では効率的に解決できない鳩の巣問題など、一部の問題では非常に効率的ですが、ほとんどの問題では遅くなります。
Gophersat で切断面を使用できるようになりました。 -cpコマンドライン オプションを使用するだけです。したがって、呼び出す代わりに次のようにします。
gophersat problem.opb
電話するだけです:
gophersat -cp problem.opb
Gophersat の最後の安定バージョンはバージョン 1.3 です。これはマイナー アップデートであり、MAXSAT 問題を処理するときに基礎となるソルバーにアクセスする機能を追加します。
Gophersat バージョン 1.2 には、問題が UNSAT である場合に RUP 証明書を提供することと、式の不満足なサブセットを抽出する機能を提供することによって、UNSAT インスタンスを理解する方法が含まれています。いくつかのバグも修正され、増分 SAT 解決のサポートが改善されました。
これらの機能の詳細については、UNSAT 証明書と MUS に関するチュートリアルを確認してください。
gophersat 実行可能ファイルで証明書を生成するには、次のように呼び出すだけです。
gophersat -certified problem.cnf
証明書は、RUP 表記を使用して標準出力に出力されます。証明書はその場で生成されるため、実際に問題が解決できる場合でも、部分的で役に立たない証明書が生成されることに注意してください。これはコミュニティでは一般的な慣行であり、生成された条項は無用なノイズですが、実際には問題ありません。
UNSAT インスタンスから MUS を抽出するには、次を呼び出すだけです。
gophersat -mus problem.cnf
MUS は標準出力に出力されます。問題が UNSAT でない場合は、エラー メッセージが表示されます。
現時点では、これらの機能は純粋な SAT 問題 (つまり、疑似ブール問題ではない) に対してのみ使用できます。
Gophersat には、バージョン 1.1 以降、純粋な SAT 問題に対する新しいより効率的なコア ソルバーと、MAXSAT 問題を扱うパッケージが含まれています。また、最適化とモデルカウントのための新しい API も含まれており、新しいモデルが見つかるとすぐにチャネルに書き込まれます。
バージョン 1.0 以降、Gophersat の API は安定していると考えられています。これは、API がメジャー バージョンに移行するまで下位互換性が維持されることが保証されていることを意味します。つまり、プログラムが gophersat のバージョン 1.0 で動作する場合、バージョン 1.1 以降でも動作しますが、必ずしも 2.0 以降のバージョンでは動作するとは限りません。
「まだ動作している」とは、「コンパイルして同じ出力が生成される」ことを意味するだけであり、「メモリや時間の点で同じパフォーマンスが得られる」ということではないことに注意してください。これは重要な違いです。マイナー バージョンのアップグレード中に、新しいヒューリスティックまたはデータ型が導入される可能性があります。これは、特定の問題の解決が以前より速くなったり、遅くなったりする可能性があることを意味します。
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat は、スタンドアロン ソルバー (DIMACS CNF ファイルの読み取り) として、または Go プログラムのライブラリとして使用できます。
DIMACS ファイルを解決するには、次の構文を使用して gophersat を呼び出すことができます。
gophersat --verbose file.cnf
--verboseは、解決プロセス中にソルバーに情報を表示させるオプションのパラメーターです。
Gophersat は、使いにくい DMACS 形式で表現された問題だけでなく、より一般的なブール式を読み取って解くこともできます。また、カーディナリティ制約、つまり、少なくとも n 個のリテラルが true (n > 1) でなければならない句もネイティブに処理します。
Gophersat は、スタンドアロンのソルバー (OPB ファイルの読み取り) として、または Go プログラムのライブラリとして使用できます。
疑似ブール問題 (決定の問題でも最適化の問題でも) を解決するには、次の構文を使用して gophersat を呼び出すことができます。
gophersat --verbose file.opb
--verboseは、解決プロセス中にソルバーに情報を表示させるオプションのパラメーターです。
現時点では、いわゆる DEC-SMALLINT-LIN 問題と OPT-SMALLINT-LIN、つまり小さな整数の線形制約 (重み付きリテラルの合計) に対する決定問題 (解があるかどうか) のみを解決できます。 (n < 2^30)、または小さな整数の線形制約に対する最適化問題 (与えられたコスト関数を最小化する最良の解決策は何か)。
maxsatパッケージのおかげで、Gophersat は MAXSAT の問題を解決できるようになりました。
重み付き MAXSAT 問題を解決するには、次の構文を使用して gophersat を呼び出すことができます。
gophersat --verbose file.wcnf
--verboseは、解決プロセス中にソルバーに情報を表示させるオプションのパラメーターです。ファイルは (WCNF 形式)[http://www.maxsat.udl.cat/08/index.php?disp=requirements] で表現されることになっています。
SAT はブール充足可能性問題の略で、標準的な NP 完全問題、つまり、最悪の場合でも指数関数的な時間がかからない既知の解が存在しない問題です。簡単に言うと、SAT ソルバーは、与えられた命題式に対して、そのすべての変数に対する代入が存在する場合、それを真にする代入を見つけようとします。
素朴なアルゴリズムを使用して SAT ソルバーを実装するのは簡単ですが、そのような実装は実際には非常に非効率的です。 Gophersat は最先端の機能を実装しているため非常に効率的で、効率的な推論エンジンを必要とする Go プログラムで実際に使用できます。
実際的な理由から、これが常に最善の決定であるとは限りませんが、NP 完全問題はすべて SAT 問題として変換でき、Gophersat によって解決できます。このような問題には、巡回セールスマン問題、制約プログラミング、ナップザック問題、計画、モデル チェック、ソフトウェアの正当性チェックなどが含まれます。
SAT 問題の詳細については、ウィキペディアの SAT に関する記事を参照してください。
また、チュートリアル「SAT for noobs」では、独自のブール式を表現して gophersat で使用できるようにする方法についても説明しています。
MAXSAT は、SAT 決定問題に相当する最適化です。純粋な SAT ソルバーはすべての節を満たすモデルを返すか、そのようなモデルが存在しない場合は UNSAT を返しますが、MAXSAT ソルバーはできるだけ多くの節を満たすモデルを返します。
MAXSAT には拡張機能があります。
部分的な MAXSAT は、できるだけ多くの条項を満たす必要があるものの、一部の条項 (ハード条項と呼ばれる) は何であっても満たさなければならないことを意味します。したがって、部分的な MAXSAT 問題は満足できないと宣言できます。
たとえば、学校の時間割の生成は、部分的な MAXSAT 問題です。ソフト (たとえば、午後 4 時以降に開始するクラスをできるだけ少なくしたい) とハード (2 人の教師が 2 つの異なる場所にいることはできない) の両方があります。同時に）制約。
加重 MAXSAT は、条項がコストに関連付けられていることを意味します。オプションではありますが、一部の条項は他の条項よりも重要であると見なされます。たとえば、条項 C1 のコストが 3 で、条項 C2 と C3 のコストが両方とも 1 の場合、C1 は満たすが C2 も C3 も満たさない解決策は、C2 と C3 の両方を満たすが C1 を満たさない解決策よりも優れているとみなされます。物事が平等であること。
部分的に重み付けされた MAXSAT は、問題にソフト節とハード節の両方があり、ソフト節が重み付けされていることを意味します。この点に関して、「純粋な」MAXSAT は、より一般的な部分重み付け MAXSAT の特定のケースです。「純粋な」MAXSAT 問題は、すべての文節が重み 1 に関連付けられたソフト文節である部分重み付け MAXSAT 問題です。
擬似ブール問題は、ある意味、SAT 問題を一般化したものです。どの命題句も単一の擬似ブール制約として記述できますが、擬似ブール制約を表すには、指数関数的な数の命題句が必要になる場合があります。
(線形) 擬似ブール式は、次のような式です。
w1 l1 + w2 x2 + ... + wn xn ≥ y
ここで、 yとすべてのwiは整数定数、すべてのliはブール リテラルです。
たとえば、次の式が真である場合、
2 ¬x1 + x2 + x3 ≥ 3
ブール変数x1 false でなければならず、 x2とx3の少なくとも 1 つは true でなければなりません。これは次の命題式に相当します。
¬x1 ∧ (x2 ∨ x3)
疑似ブール式は、命題句 (任意の句) を一般化したものです。
x1 ∨ x2 ∨ ... ∨ xn
次のように書き換えることができます
x1 + x2 + ... + xn ≥ 1
擬似ブール問題の記述は、対応する命題よりも指数関数的に小さくなる可能性がありますが、擬似ブール問題の解決は依然として NP 完全です。
Gophersat は、決定問題 (そもそも問題に対する解決策はあるのか) と最適化問題の両方を解決します。最適化問題は、コスト関数、つまり最小化する必要がある項の合計に関連付けられた擬似ブール問題です。 gophersat は、単に与えられた制約を満たすモデルを見つけようとするのではなく、制約を満たしコスト関数を最小化することが保証されているモデルを見つけようとします。
最適解の探索中、gophersat は次善の解 (つまり、すべての制約を解決するが最適であることがまだ保証されていない解) を見つけるとすぐに提供するため、ユーザーは一定の時間内に次善の解を得ることができます。制限するか、最適なソリューションが保証されるまでさらに長く待ちます。
はい、いいえ。これは単純な実装よりもはるかに高速で、現実世界の問題で使用できるほど高速ですが、高度に最適化された最先端のトップレベルのソルバーよりは遅くなります。
Gophersat は、利用可能な中で最速の SAT/PB ソルバーになることを目指しているわけではありません。目標は、他の言語 (通常は C/C++) で書かれたソルバーへのインターフェイスに頼ることなく、ゴーファーに SAT および PB テクノロジーへのアクセスを提供することです。
ただし、場合によっては、別の言語で書かれたソルバーとのインターフェースがアプリケーションにとって最適な選択となることがあります。解決すべき小さな問題がたくさんある場合は、Gophersat が最も早い代替手段になります。より大きな問題の場合、解決時間を犠牲にして依存関係をできるだけ少なくしたい場合は、Gophersat も適しています。難しい問題を解決する必要があり、cgo の使用や外部プログラムの使用を気にしない場合、Gophersat はおそらく最良の選択肢ではありません。
Go には他にもいくつかの SAT ソルバーがあり、主に go-sat と gini です。私たちが実行したテストによると、Gini のパフォーマンスは Gophersat とほぼ同等ですが、平均では少し遅いです。
Gophersat は、他のソルバーでは必ずしも利用できない優れた機能 (ユーザーフレンドリーな入力形式など) も提供しているため、SAT/PB に簡単に還元できる NP 困難な問題を記述および解決するためのツールとして使用できます。問題。
いいえbf (「ブール式」の略) パッケージは、ブール式を CNF に変換する機能を提供します。
これはモデルカウントとして知られており、そのための関数solver.Solver.CountModelsがあります。
コマンドラインからモデルをカウントすることもできます。
gophersat --count filename
ここで、filename は .opb または .cnf ファイルです。
