はじめに
Kinx で Package Manager を作ろうと思い、バージョン依存性チェックを SAT ソルバ―にやらせようと思いました。しかし複数バージョン共存できる方が良いのでは、と、バージョン依存性チェックいらないかも、と思い始めた今日この頃。結局作ったけど使わないかも、な感じになってます。
とはいえ、せっかく実装したのでいくつか遊んでみました。8 Queens と数独を解いてみます。
ちなみに Kinx とは↓コレです。
- 参考
- 最初の動機 ... スクリプト言語 KINX（ご紹介）
- 個別記事へのリンクは全てここに集約してあります。
- リポジトリ ... https://github.com/Kray-G/kinx
- Pull Request 等お待ちしております。
- 最初の動機 ... スクリプト言語 KINX（ご紹介）
また、最後に（これもせっかくなので）バージョン依存性チェックプログラムを載せておきます。使わないかもですが。
SAT ソルバ―とは
ご注意： SAT ソルバーは v1.0.0 のリリース版には含まれていません。最新の master ブランチに含まれています。
充足可能性問題を解く機械（プログラム）。Wikipedia が詳しいのでご参考。Kinx では picosat をバックエンドに使いました。
簡単に言うと、$(x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2)$ みたいな論理式があって、この式全体が真となる各変数の真偽値の組合せを見つけるというものです。例えばこの例の場合、$x_1 = $ 真、$x_2 = $ 偽とすれば全体が真となるのでこの組合せは解の一つです。
SAT ソルバ―を使う、というのは、与えられた問題を上記のような論理式で表し、SAT ソルバーに解かせ、出てきた結果を解釈する、ということを行うこと、意味します。
ちなみに、論理式の形は $(A \lor B \lor \ldots) \land (X \lor Y \lor \ldots) \land ...$ と OR でつながった式を AND でつなげた式として表現します。また、ある命題を解く際に、$A \Rightarrow B$ （$A$ ならば $B$）の条件を考えるシーンがよくありますが、これは論理式として同一の解となる $\lnot A \lor B$ で置き換えて考えます。
Kinx で使うには、以下のように using します。また、ライブラリは Satisfiablity クラスで、インスタンス化しておきましょう。
using SatisfiablitySolver;
var s = new Satisfiablity();
8 Queens を解いてみた
8 Queens を解いてみましょう。8 Queens に関しても Wikipedia が詳しいのでご参考。
SAT ソルバ―を使うということは、8 Queens の問題を論理式で表すということです。どう表せばよいでしょう。
SAT ソルバーでは、各変数を整数で管理します。そして、変数 1 が真の場合は +1、偽の場合は -1 として符号で判断できるようにします。従って、全ての状態を変数として番号を付け、ある変数（番号）が真（プラス）の時に他の変数（番号）がどうなるのかを論理式で表すようにします。こんな感じです。
- 変数
- すべてのマスを表す変数を仮定する。8 x 8 マスなので、64 個の変数がある。
- 変数が真の場合は Queen が存在するものとする。
- 条件（制約）
- 行（列でも良い）の中に少なくとも 1 つは Queen が存在する。
- ある $(i, j)$ 座標に Queen があるとした場合、その上下左右、ナナメ全てに Queen は存在しない。
この時、例えば最初の条件として 1 行目を考えます。1行目を表す変数を $x_1$, $x_2$, $x_3$, $\ldots$, $x_8$ とすると、$(x_1 \lor x_2 \lor x_3 \lor x_4 \lor x_5 \lor x_6 \lor x_7 \lor x_8)$ となります。2 ～ 8 行目も同じように条件が書けます。
プログラム的には、これを配列で表して、[1, 2, 3, 4, 5, 6, 7, 8] と扱います。全部真なのでプラスです。この 1 つの OR の式を節（Clause）と言います。複数の節を作って条件を絞っていきます。
まず、分かりやすくするために、ある $(i, j)$ の変数の番号を返す関数を作っておきましょう。ここで N は 8 です。+1 するのは、変数は 1 始まりだからです。
const N = 8;
function getVarNum(i, j) {
return (i + j * N) + 1;
}
では各行に少なくとも 1 つは Queen が存在する、というのを書くと以下のようになります。これで [1, 2, 3, 4, 5, 6, 7, 8] ～ [57, 58, 59, 60, 61, 62, 63, 64] までの 8 つの節が登録されます。
for (var jx = 0; jx < N; ++jx) {
s.addClause(N.times().map { => getVarNum(_1, jx) });
}
次の条件「ある $(i, j)$ 座標に Queen があるとした場合、その上下左右、ナナメ全てに Queen は存在しない。」はどう表しましょう。これは、$A \Rightarrow B$ の形で個別に指定していきます。例えば、「$(0, 0)$ にあれば $(1, 0)$ には存在しない」は変数で表すと、$x_1 \Rightarrow \lnot x_2$ なので、$\lnot x_1 \lor \lnot x_2$ です。つまり、節としては [-1, -2] になります。すべてのマスで上下左右、ナナメそれぞれ同じように節を追加していきます。
ところで、実は $x_1 \Rightarrow \lnot x_2$ は $x_2 \Rightarrow \lnot x_1$ と同じことを表しています。なぜなら OR は交換可能なのでどちらも $\lnot x_1 \lor \lnot x_2$ だからです。ということで、左上から順にスキャンする場合、あるマス $(i, j)$ の条件を調べる際は既に設定した節と同じものを設定する必要はありません。つまり、右、下、右下、左下、だけをスキャンして節を登録すればよいのです。
これをプログラムにすると、以下のようになります。これをすべてのマスで呼びます。
function addClauses(s, i, j) {
const ijQ = getVarNum(i, j);
/* right */
for (var ix = i + 1; ix < N; ++ix) {
s.addClause([-ijQ, -getVarNum(ix, j)]);
}
/* down */
for (var jx = j + 1; jx < N; ++jx) {
s.addClause([-ijQ, -getVarNum(i, jx)]);
}
/* right-down */
for (var ix = i + 1, jx = j + 1; ix < N && jx < N; ++ix, ++jx) {
s.addClause([-ijQ, -getVarNum(ix, jx)]);
}
/* left-down */
for (var ix = i - 1, jx = j + 1; ix >= 0 && jx < N; --ix, ++jx) {
s.addClause([-ijQ, -getVarNum(ix, jx)]);
}
}
for (var ix = 0; ix < N; ++ix) {
for (var jx = 0; jx < N; ++jx) {
addClauses(s, ix, jx);
}
}
さて、ここまで準備できたら SAT ソルバーから解を求めます。Satisfiablity クラスはイテレータブルにしてあるので、以下のように for-in で回せます。
function display(e) {
System.print("\nSolution %d\n" % ++solution);
var board = [];
for (var ijQ = 0, l = e.length(); ijQ < l; ++ijQ) {
var i = ijQ % N;
var j = Integer.parseInt(ijQ / N);
board[i][j] = e[ijQ] > 0;
}
for (var jx = 0; jx < N; ++jx) {
for (var ix = 0; ix < N; ++ix) {
System.print(board[ix][jx] ? " Q" : " .");
}
System.println("");
}
}
for (var e in s) {
display(e);
}
実行すると、無事 92 個の解が表示されました。
$ ./kinx examples/sat_nqueens.kx
Solution 1
. . . . . . . Q
. Q . . . . . .
. . . . Q . . .
. . Q . . . . .
Q . . . . . . .
. . . . . . Q .
. . . Q . . . .
. . . . . Q . .
Solution 2
. . . Q . . . .
. . . . . . . Q
. . . . Q . . .
. . Q . . . . .
Q . . . . . . .
. . . . . . Q .
. Q . . . . . .
. . . . . Q . .
/* 省略 */
Solution 92
. . . Q . . . .
. . . . . . Q .
. . . . Q . . .
. Q . . . . . .
. . . . . Q . .
Q . . . . . . .
. . Q . . . . .
. . . . . . . Q
数独を解いてみた
次に数独を解いてみます。数独に関してもまた Wikipedia が詳しいのでご参考。
数独は変数の数が増えます。縦横に加えてマスごとに 1 ～ 9 までの数値を取るといった奥行的な（立体的な）イメージを持つ必要がありますが、考え方は一緒です。
各マスが １ ～ 9 までの数値を取るので、マスごとに 9 個の状態を持たせます。つまり、左上のマスが 1 であるとき、2 であるとき、... と全て異なる変数として扱います。例えば、$R \times R$ の数独において $(i, j)$ が $v$ であるときの変数の番号を $(i + j \times R) \times R + v$ として定義します。$v$ が 1 から始まるので 1 加える必要はありません。例えば、変数 1 が真であれば、左上のマスは 1 です。変数 9 が真であれば、左上のマスは 9 であることを表します。変数 10 はマスが移って、左上の 1 つ右（左から 2 番目）のマスが 1 ということになります。
では早速先ほどと同様に、変数の番号を返す関数から定義してみましょう。$R \times R$ の数独です。
function getVarNum(i, j, v) {
return ((i + j * R) * R) + v;
}
次に制約条件です。「ミニ区画」と言ってますが、$9 \times 9$ の数独の場合、その中に 9 つ存在する $3 \times 3$ の領域のことを意味しています。この 3 を $N$ とします。つまり、$R = N^{2}$ です。
- あるマス $(i, j)$ には 1 ～ 9 のいずれかの数値が入る。
- あるマス $(i, j)$ が $v$ であるとき、同じ $(i, j)$ のマスには $v$ 以外の数値は存在しない。
- あるマス $(i, j)$ が $v$ であるとき、同じ行に $v$ は存在しない。
- あるマス $(i, j)$ が $v$ であるとき、同じ列に $v$ は存在しない。
- あるマス $(i, j)$ が $v$ であるとき、そのマスを含むミニ区画に $v$ は存在しない。
これをプログラムで書くと、次のようになります。
function addClauses(s, i, j, v) {
const ijv = getVarNum(i, j, v);
// There is at most one number in each cell. (Cell - uniqueness)
for (var vi = 1; vi <= R; ++vi) {
if (v != vi) {
s.addClause([-ijv, -getVarNum(i, j, vi)]);
}
}
// Each number appears at most once in each row. (Row - uniqueness)
for (var ix = i + 1; ix < R; ++ix) {
s.addClause([-ijv, -getVarNum(ix, j, v)]);
}
// Each number appears at most once in each column. (Column - uniqueness)
for (var jx = j + 1; jx < R; ++jx) {
s.addClause([-ijv, -getVarNum(i, jx, v)]);
}
var si = Integer.parseInt(i / N) * N; // i as a left top in sub square.
var sj = Integer.parseInt(j / N) * N; // j as a left top in sub square.
var ei = si + N;
var ej = sj + N;
// Each number appears at most once in each block. (Block - uniqueness)
for (var ix = si; ix < ei; ++ix) {
for (var jx = sj; jx < ej; ++jx) {
const ijv2 = getVarNum(ix, jx, v);
if (ijv2 > ijv) {
s.addClause([-ijv, -ijv2]);
}
}
}
}
for (var j = 0; j < R; ++j) {
for (var i = 0; i < R; ++i) {
const ijv = ((i + j * R) * R);
var v = test[j][i];
if (v == 0) {
// There is at least one number in each cell. (Cell - definedness)
s.addClause(R.times().map { => ijv + (_1 + 1) });
} else {
s.addClause([ ijv + v ]);
}
R.times().each { => addClauses(s, i, j, (_1 + 1)) };
}
}
実際に $9 \times 9$ の数独を解いてみましょう。
+----------+----------+----------+
| 8 . . | . . . | . . . |
| . . 3 | 6 . . | . . . |
| . 7 . | . 9 . | 2 . . |
+----------+----------+----------+
| . 5 . | . . 7 | . . . |
| . . . | . 4 5 | 7 . . |
| . . . | 1 . . | . 3 . |
+----------+----------+----------+
| . . 1 | . . . | . 6 8 |
| . . 8 | 5 . . | . 1 . |
| . 9 . | . . . | 4 . . |
+----------+----------+----------+
↓
+----------+----------+----------+
| 8 1 2 | 7 5 3 | 6 4 9 |
| 9 4 3 | 6 8 2 | 1 7 5 |
| 6 7 5 | 4 9 1 | 2 8 3 |
+----------+----------+----------+
| 1 5 4 | 2 3 7 | 8 9 6 |
| 3 6 9 | 8 4 5 | 7 2 1 |
| 2 8 7 | 1 6 9 | 5 3 4 |
+----------+----------+----------+
| 5 2 1 | 9 7 4 | 3 6 8 |
| 4 3 8 | 5 2 6 | 9 1 7 |
| 7 9 6 | 3 1 8 | 4 5 2 |
+----------+----------+----------+
解けました。
ところが、これでもいいのですが、実は $25 \times 25$ の数独で返ってきません。実は冗長であっても節を増やしたほうが余計な条件を枝刈りして速く解を得ることができたりします。ここでは、以下の条件を追加してみます。
- 各数値は、少なくとも 1 つは各行に存在する。
- 各数値は、少なくとも 1 つは各列に存在する。
プログラムで書くとこんな感じです。
for (var v = 1; v <= R; ++v) {
// Each number appears at least once in each row. (Row - definedness)
for (var j = 0; j < R; ++j) {
s.addClause(R.times().map { => getVarNum(_1, j, v) });
}
// Each number appears at least once in each column. (Column - definedness)
for (var i = 0; i < R; ++i) {
s.addClause(R.times().map { => getVarNum(i, _1, v) });
}
}
これを加えると、$25 \times 25$ の数独も 1 秒未満で答えが得られました！
+----------------+----------------+----------------+----------------+----------------+
| . 12 . . . | . . . . . | . . . 9 . | . . 15 . . | 22 . . . . |
| . . . . . | . 9 . 19 . | . . 10 11 . | . . . . . | . . . . . |
| . 4 . 22 . | . . . . . | . . . . . | . . 12 . . | 20 15 1 . . |
| 16 1 20 15 . | . . . . . | . . . . . | 14 . 4 . 22 | 12 25 . . . |
| . . . . . | . 7 2 11 . | 23 . 19 8 . | . . . 13 . | . . . . . |
+----------------+----------------+----------------+----------------+----------------+
| 13 . 8 . 2 | . . . . . | . . 7 23 6 | . 9 . 19 11 | . . . . . |
| . . . . 23 | . . . . 16 | . . . . . | . . . . . | 1 . . . . |
| 7 . . . 10 | 3 . . . . | . . 9 19 . | . 13 . 23 . | . . . 5 . |
| . . . . . | 15 . . . 22 | . . . . . | . . . . . | 25 20 . . . |
| . . . . . | 12 . 14 1 25 | . . . . . | . . 3 . . | 16 4 15 . . |
+----------------+----------------+----------------+----------------+----------------+
| . . . . . | . 19 9 . . | . . 13 7 . | . . . 5 . | . . . 23 10 |
| . 22 . 25 17 | . . . . . | . . . . . | 12 . 20 . . | . . . . . |
| . 20 12 16 . | . . . . . | . . . . 14 | 15 22 1 . 25 | . . . . . |
| . 15 . . . | . 11 . . . | . . . . . | . . 16 . . | . . . 9 . |
| . . . 1 . | . 10 . 23 . | . . . . 18 | . . . . . | . . . . 8 |
+----------------+----------------+----------------+----------------+----------------+
| 10 . . . 8 | . 13 . 5 . | . . . . . | . 19 . 11 23 | . . . 6 . |
| . . . 17 7 | . . . . . | . . . . 1 | . . . . . | 4 22 . . . |
| . . . . 11 | . 23 . . . | . . . . 20 | . . . 2 . | 14 . . . . |
| 19 . 23 . 5 | . 8 . 9 . | . 21 . . . | . 10 . 7 . | . . . . . |
| . 3 . . . | . . . . . | 25 4 . . 12 | . . . . . | 15 1 16 . . |
+----------------+----------------+----------------+----------------+----------------+
| . . . . . | . . . . 15 | . 12 . . 25 | 1 . 22 . . | 3 . . . . |
| 23 . . . 19 | . 2 . . . | . . . . . | . . . 10 . | . . . 7 11 |
| . . . 18 . | . . . . . | . 20 . . . | . . . . . | . . . . . |
| . . . . . | . . . . 4 | 14 15 . . 22 | . . . . . | . . . 10 . |
| 11 . . . 9 | . . . . . | . . . . . | . . . . . | . . . 19 . |
+----------------+----------------+----------------+----------------+----------------+
↓
+----------------+----------------+----------------+----------------+----------------+
| 8 12 11 10 18 | 14 25 4 16 24 | 20 17 1 9 21 | 19 5 15 6 2 | 22 23 7 3 13 |
| 2 23 13 7 25 | 22 9 15 19 20 | 12 24 10 11 4 | 17 16 18 1 3 | 8 6 5 14 21 |
| 9 4 19 22 21 | 13 3 18 17 5 | 16 6 25 14 7 | 23 11 12 8 10 | 20 15 1 24 2 |
| 16 1 20 15 24 | 10 21 6 8 23 | 5 2 18 3 13 | 14 7 4 9 22 | 12 25 11 17 19 |
| 14 5 17 6 3 | 1 7 2 11 12 | 23 22 19 8 15 | 21 25 24 13 20 | 10 9 18 16 4 |
+----------------+----------------+----------------+----------------+----------------+
| 13 25 8 4 2 | 18 20 21 24 10 | 15 1 7 23 6 | 16 9 5 19 11 | 17 3 14 22 12 |
| 22 24 3 21 23 | 9 17 19 13 16 | 18 14 20 25 5 | 6 12 2 15 4 | 1 10 8 11 7 |
| 7 14 15 12 10 | 3 4 8 2 11 | 22 16 9 19 17 | 20 13 25 23 1 | 6 24 21 5 18 |
| 17 11 16 5 1 | 15 6 23 7 22 | 3 13 4 12 8 | 18 21 10 14 24 | 25 20 19 2 9 |
| 6 9 18 19 20 | 12 5 14 1 25 | 2 10 21 24 11 | 7 17 3 22 8 | 16 4 15 13 23 |
+----------------+----------------+----------------+----------------+----------------+
| 3 8 2 11 4 | 20 19 9 15 18 | 1 25 13 7 16 | 24 6 14 5 17 | 21 12 22 23 10 |
| 5 22 10 25 17 | 2 1 3 4 13 | 8 11 6 21 19 | 12 23 20 18 9 | 7 14 24 15 16 |
| 18 20 12 16 13 | 8 24 5 6 7 | 9 23 17 10 14 | 15 22 1 21 25 | 19 11 2 4 3 |
| 24 15 7 23 14 | 21 11 25 12 17 | 4 5 22 20 2 | 10 8 16 3 19 | 13 18 6 9 1 |
| 21 19 9 1 6 | 16 10 22 23 14 | 24 3 12 15 18 | 11 2 7 4 13 | 5 17 20 25 8 |
+----------------+----------------+----------------+----------------+----------------+
| 10 16 1 14 8 | 25 13 12 5 2 | 17 18 15 22 24 | 4 19 21 11 23 | 9 7 3 6 20 |
| 12 2 25 17 7 | 6 15 24 18 21 | 10 19 11 13 1 | 3 14 9 20 16 | 4 22 23 8 5 |
| 15 21 4 13 11 | 17 23 16 22 3 | 7 9 8 5 20 | 25 1 6 2 12 | 14 19 10 18 24 |
| 19 18 23 24 5 | 4 8 20 9 1 | 6 21 14 16 3 | 22 10 17 7 15 | 11 2 13 12 25 |
| 20 3 6 9 22 | 11 14 7 10 19 | 25 4 23 2 12 | 13 18 8 24 5 | 15 1 16 21 17 |
+----------------+----------------+----------------+----------------+----------------+
| 4 10 5 8 16 | 23 18 11 21 15 | 19 12 2 6 25 | 1 24 22 17 7 | 3 13 9 20 14 |
| 23 17 22 20 19 | 24 2 1 25 6 | 21 8 3 4 9 | 5 15 13 10 14 | 18 16 12 7 11 |
| 25 13 21 18 15 | 7 12 10 14 9 | 11 20 24 17 23 | 8 3 19 16 6 | 2 5 4 1 22 |
| 1 7 24 2 12 | 19 16 13 3 4 | 14 15 5 18 22 | 9 20 11 25 21 | 23 8 17 10 6 |
| 11 6 14 3 9 | 5 22 17 20 8 | 13 7 16 1 10 | 2 4 23 12 18 | 24 21 25 19 15 |
+----------------+----------------+----------------+----------------+----------------+
尚、サンプルプログラムでは答えに色を付けて、元々あった数値と区別できるようにしています。こんな感じです。
バージョン依存性チェックを作ってみた
さて、当初の目的の本命です。使わないかもしれませんが。
製品（プロダクト）とバージョンの組合せを変数にして、問題を解かせて組合せとして真となるかを判断するのは一緒です。番号付けが登録順で対処する感じですが、まぁ考え方は一緒です。ただ、バージョンチェックに関していうとこれまでと違うところがあります。それは 偽となったときに何が悪かったのか を教えてあげないといけないのです。どの版数とどの版数がコンフリクトしているのか、と。
これは、これまでのやり方だけではできません。ここでは picosat の機能を使って実現しました。picosat には MUS（Minimally Unsatisfiable Subformulas）というものを見つける仕組みがあり、これを使います。
バージョンチェックには特別に用意した VersionSatisfiablity クラスを使います。
var vs = new VersionSatisfiablity();
製品 X のバージョン 0.0.1 がターゲットです。製品 A, B, Z はそれぞれバージョン 0.0.1 と 0.0.2 が存在します。
var X = vs.addProduct("X")
.addVersion("0.0.1", true);
var A = vs.addProduct("A")
.addVersion("0.0.1")
.addVersion("0.0.2");
var B = vs.addProduct("B")
.addVersion("0.0.1")
.addVersion("0.0.2");
var Z = vs.addProduct("Z")
.addVersion("0.0.1")
.addVersion("0.0.2");
ここで、製品 A, B, Z の依存関係を定義します。ここでは単純に同じバージョンで依存する感じで A と B が Z に依存するものとします。
A("0.0.1").dependsOn(Z("0.0.1"));
A("0.0.2").dependsOn(Z("0.0.2"));
B("0.0.1").dependsOn(Z("0.0.1"));
B("0.0.2").dependsOn(Z("0.0.2"));
ここで、X が A と B に依存し、どちらも同じ版数に依存していれば問題無いですね。やってみましょう。
X("0.0.1").dependsOn(A("0.0.2"));
X("0.0.1").dependsOn(B("0.0.2"));
tryit();
ちなみに tryit() は結果を出すものですが、その定義は重要ではないので後程お見せします。今回は結果だけ。ちゃんと定義した依存関係の版数で問題無し、という結果になりました。
1: [{
"index": 1,
"isFix": 1,
"name": "X",
"version": "0.0.1"
}, {
"index": 3,
"isFix": null,
"name": "A",
"version": "0.0.2"
}, {
"index": 5,
"isFix": null,
"name": "B",
"version": "0.0.2"
}, {
"index": 7,
"isFix": null,
"name": "Z",
"version": "0.0.2"
}]
条件を変えて、B の 0.0.1 に依存するようにしてみましょう。
X("0.0.1").dependsOn(A("0.0.2"));
X("0.0.1").dependsOn(B("0.0.1"));
tryit();
こうなりました。
Unsatisfiable - Conflict here
- X is v0.0.1
- Z is v0.0.1 => Z is NOT v0.0.2
- A is v0.0.2 => Z is v0.0.2
- B is v0.0.1 => Z is v0.0.1
- X is v0.0.1 => A is v0.0.2
- X is v0.0.1 => B is v0.0.1
これは、以下の組合せが満たせない、と伝えています。今回はほぼほぼ全部出てしまってますが、条件が複雑になると満たせなかった条件だけが出力されます。
- X が 0.0.1 であること
- Z の 0.0.1 と 0.0.2 が排他であること
- A が 0.0.2 のとき Z が 0.0.2 であること
- B が 0.0.1 のとき Z が 0.0.1 であること
- X が 0.0.1 のとき A が 0.0.2 であること
- X が 0.0.1 のとき B が 0.0.1 であること
おわりに
せっかく SAT ソルバー入れてみたのでどこかで使えるといいな。パズルを解かせるのはちょっと面白かった。
そして本題の Package Manager はどうやって実現しようか考え中です。
P.S. tryit() の定義
function msg(a) {
if (a.not) {
return ("%1% is NOT v%2%" % a.value.name % a.value.version).format();
} else {
return ("%1% is v%2%" % a.value.name % a.value.version).format();
}
}
function error(item) {
switch (item.length()) {
when 1:
System.println("- ", msg(item[0]));
when 2:
item[0].not = !item[0].not; // (!A || B) means (A => B)
System.println("- ", msg(item[0]), " => ", msg(item[1]));
else:
System.println("- ", item.map { => msg(_1) }.join(', or\n '));
}
}
function tryit() {
var count = 0;
for (var e in vs) {
System.println("%d: " % ++count, e.toJsonString(true));
}
if (count == 0) {
System.println("Unsatisfiable - Conflict here");
vs.getConflict().each { => error(_1) };
}
}