🍺

CNFの組み立て方を思い出す話

2021/10/29に公開

sat

cnf

tech

そもそもCNFって何だっけ？

CNF

連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）
ってwikipediaに書いてました。

乱暴に言えば、

リテラル単体もしくはリテラルを論理積で羅列したもの
論理積を構成する各リテラルはリテラル単体もしくはリテラルを論理和で羅列したもの
リテラル単体にのみ否定が許可されている

なんか面倒そうですけど、これが書けるとSAT solverが使えます。
SATisfiability problem/充足可能性問題のsolver/解決機ですね。

今回はナンプレを解く為のCNFを作成します。

ナンプレを解くCNFを組み立てる

数独/ナンバープレース

以下wikipediaよりルールを抜粋
3×3のブロックに区切られた 9×9の正方形の枠内に1〜9までの数字を入れるペンシルパズルの一つである。

マスに1～9のいずれかの数字を入れる。
縦・横の各列に、同じ数字が重複して入ってはいけない。
太線で囲まれた3×3のブロック内に、同じ数字が重複して入ってはいけない。

このルールをより具体的にします。

縦軸をa-i、横軸をA-Iとして、左上をaA、右下をiIと表すことにしました。

wikipediaの例

	A	B	C	D	E	F	G	H	I
a	5	3			7
b	6			1	9	5
c		9	8					6
d	8				6				3
e	4			8		3			1
f	7				2				6
g		6					2	8
h				4	1	9			5
i					8			7	9

早見表

	A	B	C	D	E	F	G	H	I
a	aA	aB	aC	aD	aE	aF	aG	aH	aI
b	bA	bB	bC	bD	bE	bF	bG	bH	bI
c	cA	cB	cC	cD	cE	cF	cG	cH	cI
d	dA	dB	dC	dD	dE	dF	dG	dH	dI
e	eA	eB	eC	eD	eE	eF	eG	eH	eI
f	fA	fB	fC	fD	fE	fF	fG	fH	fI
g	gA	gB	gC	gD	gE	gF	gG	gH	gI
h	hA	hB	hC	hD	hE	hF	hG	hH	hI
i	iA	iB	iC	iD	iE	iF	iG	iH	iI

マスに1～9のいずれかの数字を入れる。
- aAは1～9のいずれかの数字を入れる
- aBは1～9のいずれかの数字を入れる
- aCは1～9のいずれかの数字を入れる
- aDは1～9のいずれかの数字を入れる
- aEは1～9のいずれかの数字を入れる
- aFは1～9のいずれかの数字を入れる
- aGは1～9のいずれかの数字を入れる
- aHは1～9のいずれかの数字を入れる
- aIは1～9のいずれかの数字を入れる
- bA～bI同上
- cA～iI同上
横の各列に、同じ数字が重複して入ってはいけない。
- aA,aB,aC,aD,aE,aF,aG,aH,aIの値は重複しない
- bA,bB,bC,bD,bE,bF,bG,bH,bIの値は重複しない
- c～i同上
縦の各列に、同じ数字が重複して入ってはいけない。
- aA,bA,cA,dA,eA,fA,gA,hA,iAの値は重複しない
- aB,bB,cB,dB,eB,fB,gB,hB,iBの値は重複しない
- C～I同上
太線で囲まれた3×3のブロック内に、同じ数字が重複して入ってはいけない。
- aA,aB,aC,bA,bB,bC,cA,cB,cCの値は重複しない
- aD,aE,aF,bD,bE,bF,cD,cE,cFの値は重複しない
- aG,aH,aI,bG,bH,bI,cG,cH,cIの値は重複しない
- dA,dB,dC,eA,eB,eC,fA,fB,fCの値は重複しない
- dD,dE,dF,eD,eE,eF,fD,fE,fFの値は重複しない
- dG,dH,dI,eG,eH,eI,fG,fH,fIの値は重複しない
- gA,gB,gC,hA,hB,hC,iA,iB,iCの値は重複しない
- gD,gE,gF,hD,hE,hF,iD,iE,iFの値は重複しない
- gG,gH,gI,hG,hH,hI,iG,iH,iIの値は重複しない

CNFは真偽のみを扱うので、「1～9のいずれか」を表現する為に、更に1～9で分けます。
具体的にはaA1が真ならaAは1、aA2が真ならaAは2（、3以降も同様）というルールを足します。

早見表

	A	B	C	D	E	F	G	H	I
a	aA1,aA2,aA3,aA4,aA5,aA6,aA7,aA8,aA9	aB1-9	aC1-9	aD1-9	aE1-9	aF1-9	aG1-9	aH1-9	aI1-9
b	bA1-9	bB1-9	bC1-9	bD1-9	bE1-9	bF1-9	bG1-9	bH1-9	bI1-9
c	cA1-9	cB1-9	cC1-9	cD1-9	cE1-9	cF1-9	cG1-9	cH1-9	cI1-9
d	dA1-9	dB1-9	dC1-9	dD1-9	dE1-9	dF1-9	dG1-9	dH1-9	dI1-9
e	eA1-9	eB1-9	eC1-9	eD1-9	eE1-9	eF1-9	eG1-9	eH1-9	eI1-9
f	fA1-9	fB1-9	fC1-9	fD1-9	fE1-9	fF1-9	fG1-9	fH1-9	fI1-9
g	gA1-9	gB1-9	gC1-9	gD1-9	gE1-9	gF1-9	gG1-9	gH1-9	gI1-9
h	hA1-9	hB1-9	hC1-9	hD1-9	hE1-9	hF1-9	hG1-9	hH1-9	hI1-9
i	iA1-9	iB1-9	iC1-9	iD1-9	iE1-9	iF1-9	iG1-9	iH1-9	iI1-9

マスに1～9のいずれかの数字を入れる。
- aAは1～9のいずれかの数字を入れる
  - aA1,aA2,aA3,aA4,aA5,aA6,aA7,aA8,aA9のいずれかは真である
  - aA1,aA2,aA3,aA4,aA5,aA6,aA7,aA8,aA9の二つ以上は同時に真にならない
    - aA1,aA2のどちらかもしくは両方が偽である（aA1,aA2は共に真とはならない）
    - aA1,aA3のどちらかもしくは両方が偽である
    - aA1,aA4のどちらかもしくは両方が偽である
    - aA1,aA5のどちらかもしくは両方が偽である
    - aA1,aA6のどちらかもしくは両方が偽である
    - aA1,aA7のどちらかもしくは両方が偽である
    - aA1,aA8のどちらかもしくは両方が偽である
    - aA1,aA9のどちらかもしくは両方が偽である
    - aA2,aA3のどちらかもしくは両方が偽である
    - aA2,aA4のどちらかもしくは両方が偽である
    - aA2,aA5のどちらかもしくは両方が偽である
    - aA2,aA6のどちらかもしくは両方が偽である
    - aA2,aA7のどちらかもしくは両方が偽である
    - aA2,aA8のどちらかもしくは両方が偽である
    - aA2,aA9のどちらかもしくは両方が偽である
    - aA3,aA4のどちらかもしくは両方が偽である
    - aA3,aA5のどちらかもしくは両方が偽である
    - aA3,aA6のどちらかもしくは両方が偽である
    - aA3,aA7のどちらかもしくは両方が偽である
    - aA3,aA8のどちらかもしくは両方が偽である
    - aA3,aA9のどちらかもしくは両方が偽である
    - aA4,aA5のどちらかもしくは両方が偽である
    - aA4,aA6のどちらかもしくは両方が偽である
    - aA4,aA7のどちらかもしくは両方が偽である
    - aA4,aA8のどちらかもしくは両方が偽である
    - aA4,aA9のどちらかもしくは両方が偽である
    - aA5,aA6のどちらかもしくは両方が偽である
    - aA5,aA7のどちらかもしくは両方が偽である
    - aA5,aA8のどちらかもしくは両方が偽である
    - aA5,aA9のどちらかもしくは両方が偽である
    - aA6,aA7のどちらかもしくは両方が偽である
    - aA6,aA8のどちらかもしくは両方が偽である
    - aA6,aA9のどちらかもしくは両方が偽である
    - aA7,aA8のどちらかもしくは両方が偽である
    - aA7,aA9のどちらかもしくは両方が偽である
    - aA8,aA9のどちらかもしくは両方が偽である
- 他のマスも同様
横の各列に、同じ数字が重複して入ってはいけない。
- aA,aB,aC,aD,aE,aF,aG,aH,aIの値は重複しない
  - aA1,aB1,aC1,aD1,aE1,aF1,aG1,aH1,aI1の二つ以上は同時に真にならない
    - aA1,aB1のどちらかもしくは両方が偽である（aA1,aB1は共に真とはならない）
    - aA1,aC1のどちらかもしくは両方が偽である
    - aA1,aD1のどちらかもしくは両方が偽である
    - aA1,aE1のどちらかもしくは両方が偽である
    - aA1,aF1のどちらかもしくは両方が偽である
    - aA1,aG1のどちらかもしくは両方が偽である
    - aA1,aH1のどちらかもしくは両方が偽である
    - aA1,aI1のどちらかもしくは両方が偽である
    - aB1,aC1のどちらかもしくは両方が偽である
    - aB1,aD1のどちらかもしくは両方が偽である
    - aB1,aE1のどちらかもしくは両方が偽である
    - aB1,aF1のどちらかもしくは両方が偽である
    - aB1,aG1のどちらかもしくは両方が偽である
    - aB1,aH1のどちらかもしくは両方が偽である
    - aB1,aI1のどちらかもしくは両方が偽である
    - aC1,aD1のどちらかもしくは両方が偽である
    - aC1,aE1のどちらかもしくは両方が偽である
    - aC1,aF1のどちらかもしくは両方が偽である
    - aC1,aG1のどちらかもしくは両方が偽である
    - aC1,aH1のどちらかもしくは両方が偽である
    - aC1,aI1のどちらかもしくは両方が偽である
    - aD1,aE1のどちらかもしくは両方が偽である
    - aD1,aF1のどちらかもしくは両方が偽である
    - aD1,aG1のどちらかもしくは両方が偽である
    - aD1,aH1のどちらかもしくは両方が偽である
    - aD1,aI1のどちらかもしくは両方が偽である
    - aE1,aF1のどちらかもしくは両方が偽である
    - aE1,aG1のどちらかもしくは両方が偽である
    - aE1,aH1のどちらかもしくは両方が偽である
    - aE1,aI1のどちらかもしくは両方が偽である
    - aF1,aG1のどちらかもしくは両方が偽である
    - aF1,aH1のどちらかもしくは両方が偽である
    - aF1,aI1のどちらかもしくは両方が偽である
    - aG1,aH1のどちらかもしくは両方が偽である
    - aG1,aI1のどちらかもしくは両方が偽である
    - aH1,aI1のどちらかもしくは両方が偽である
  - aA2,aB2,aC2,aD2,aE2,aF2,aG2,aH2,aI2の二つ以上は同時に真にならない
    - 同上
  - 3～9に関しても同様
- b～i同上
縦の各列に、同じ数字が重複して入ってはいけない。
- aA,bA,cA,dA,eA,fA,gA,hA,iAの値は重複しない
  - aA1,bA1,cA1,dA1,eA1,fA1,gA1,hA1,iA1の二つ以上は同時に真にならない
    - 同上
- B～I同上
太線で囲まれた3×3のブロック内に、同じ数字が重複して入ってはいけない。
- aA,aB,aC,bA,bB,bC,cA,cB,cCの値は重複しない
  - aA1,aB1,aC1,bA1,bB1,bC1,cA1,cB1,cC1の二つ以上は同時に真にならない
    - 同上
- aD,aE,aF,bD,bE,bF,cD,cE,cFの値は重複しない
  - 同上
- aG,aH,aI,bG,bH,bI,cG,cH,cIの値は重複しない
  - 同上
- dA,dB,dC,eA,eB,eC,fA,fB,fCの値は重複しない
  - 同上
- dD,dE,dF,eD,eE,eF,fD,fE,fFの値は重複しない
  - 同上
- dG,dH,dI,eG,eH,eI,fG,fH,fIの値は重複しない
  - 同上
- gA,gB,gC,hA,hB,hC,iA,iB,iCの値は重複しない
  - 同上
- gD,gE,gF,hD,hE,hF,iD,iE,iFの値は重複しない
  - 同上
- gG,gH,gI,hG,hH,hI,iG,iH,iIの値は重複しない
  - 同上

CNFは一行が論理和、行間が論理積、マイナス記号は否定を表すので、

aA1,aB1,aC1,aD1,aE1,aF1,aG1,aH1,aI1のいずれかは真である
は

aA1 aB1 aC1 aD1 aE1 aF1 aG1 aH1 aI1

aA1,aB1のどちらかもしくは両方が偽である（aA1,aB1は共に真とはならない）
は

-aA1 -aB1

（aAが1でaBも1の場合のみfalse判定になりますね）

マスに1～9のいずれかの数字を入れる。
- aAは1～9のいずれかの数字を入れる
  - aA1 aA2 aA3 aA4 aA5 aA6 aA7 aA8 aA9
  - aA1,aA2,aA3,aA4,aA5,aA6,aA7,aA8,aA9の二つ以上は同時に真にならない
    - -aA1 -aA2
    - -aA1 -aA3
    - -aA1 -aA4
    - -aA1 -aA5
    - -aA1 -aA6
    - -aA1 -aA7
    - -aA1 -aA8
    - -aA1 -aA9
    - -aA2 -aA3
    - -aA2 -aA4
    - -aA2 -aA5
    - -aA2 -aA6
    - -aA2 -aA7
    - -aA2 -aA8
    - -aA2 -aA9
    - -aA3 -aA4
    - -aA3 -aA5
    - -aA3 -aA6
    - -aA3 -aA7
    - -aA3 -aA8
    - -aA3 -aA9
    - -aA4 -aA5
    - -aA4 -aA6
    - -aA4 -aA7
    - -aA4 -aA8
    - -aA4 -aA9
    - -aA5 -aA6
    - -aA5 -aA7
    - -aA5 -aA8
    - -aA5 -aA9
    - -aA6 -aA7
    - -aA6 -aA8
    - -aA6 -aA9
    - -aA7 -aA8
    - -aA7 -aA9
    - -aA8 -aA9
- 他のマスも同様
横の各列に、同じ数字が重複して入ってはいけない。
- aA,aB,aC,aD,aE,aF,aG,aH,aIの値は重複しない
  - aA1,aB1,aC1,aD1,aE1,aF1,aG1,aH1,aI1の二つ以上は同時に真にならない
    - -aA1 -aB1
    - -aA1 -aC1
    - -aA1 -aD1
    - -aA1 -aE1
    - -aA1 -aF1
    - -aA1 -aG1
    - -aA1 -aH1
    - -aA1 -aI1
    - -aB1 -aC1
    - -aB1 -aD1
    - -aB1 -aE1
    - -aB1 -aF1
    - -aB1 -aG1
    - -aB1 -aH1
    - -aB1 -aI1
    - -aC1 -aD1
    - -aC1 -aE1
    - -aC1 -aF1
    - -aC1 -aG1
    - -aC1 -aH1
    - -aC1 -aI1
    - -aD1 -aE1
    - -aD1 -aF1
    - -aD1 -aG1
    - -aD1 -aH1
    - -aD1 -aI1
    - -aE1 -aF1
    - -aE1 -aG1
    - -aE1 -aH1
    - -aE1 -aI1
    - -aF1 -aG1
    - -aF1 -aH1
    - -aF1 -aI1
    - -aG1 -aH1
    - -aG1 -aI1
    - -aH1 -aI1
  - aA2,aB2,aC2,aD2,aE2,aF2,aG2,aH2,aI2の二つ以上は同時に真にならない
    - 同上
  - 3～9に関しても同様
- b～i同上
縦の各列に、同じ数字が重複して入ってはいけない。
- aA,bA,cA,dA,eA,fA,gA,hA,iAの値は重複しない
  - aA1,bA1,cA1,dA1,eA1,fA1,gA1,hA1,iA1の二つ以上は同時に真にならない
    - 同上
- B～I同上
太線で囲まれた3×3のブロック内に、同じ数字が重複して入ってはいけない。
- aA,aB,aC,bA,bB,bC,cA,cB,cCの値は重複しない
  - aA1,aB1,aC1,bA1,bB1,bC1,cA1,cB1,cC1の二つ以上は同時に真にならない
    - 同上
- aD,aE,aF,bD,bE,bF,cD,cE,cFの値は重複しない
  - 同上
- aG,aH,aI,bG,bH,bI,cG,cH,cIの値は重複しない
  - 同上
- dA,dB,dC,eA,eB,eC,fA,fB,fCの値は重複しない
  - 同上
- dD,dE,dF,eD,eE,eF,fD,fE,fFの値は重複しない
  - 同上
- dG,dH,dI,eG,eH,eI,fG,fH,fIの値は重複しない
  - 同上
- gA,gB,gC,hA,hB,hC,iA,iB,iCの値は重複しない
  - 同上
- gD,gE,gF,hD,hE,hF,iD,iE,iFの値は重複しない
  - 同上
- gG,gH,gI,hG,hH,hI,iG,iH,iIの値は重複しない
  - 同上

CNFは変数を1次元で扱う必要があるが、現在「縦」「横」「1-9」の3次元になっている為、
aA1 => v1, aA2 => v2, aA9 => v9, aB2 => v10, aB9 => v18, aC1 => v19, ...と1次元に置き換える。（便宜上vを付けますが、これは解説で数独の1-9との区別をつける為です。）

縦のa-iを0-8,横のA-Iを0-8とすると
（縦×9×9）＋（横×9）＋「1-9」
で計算できる。iI9 => v729

早見表

	A(0)	B(1)	C(2)	D(3)	E(4)	F(5)	G(6)	H(7)	I(8)
a(0)	v1-v9	v10-v18	v19-v27	v28-v36	v37-v45	v46-v54	v55-v64	v65-v72	v73-v81
b(1)	v82-v90	v91-v99	v100-v108	v109-v117	v118-v126	v127-v135	v136-v144	v145-v153	v154-v162
c(2)	v163-v171	v172-v180	v181-v189	v190-v198	v199-v207	v208-v216	v217-v225	v226-v234	v235-v243
d(3)	v244-v252	v253-v261	v262-v270	v271-v279	v280-v288	v289-v297	v298-v306	v307-v315	v316-v324
e(4)	v325-v333	v334-v342	v343-v351	v352-v360	v361-v369	v370-v378	v379-v387	v388-v396	v397-v405
f(5)	v406-v414	v415-v423	v424-v432	v433-v441	v442-v450	v451-v459	v460-v468	v469-v477	v478-v486
g(6)	v487-v495	v496-v504	v505-v513	v514-v522	v523-v531	v532-v540	v541-v549	v550-v558	v559-v567
h(7)	v568-v576	v577-v585	v586-v594	v595-v603	v604-v612	v613-v621	v622-v630	v631-v639	v640-v648
i(8)	v649-v657	v658-v666	v667-v675	v675-v684	v685-v693	v694-v702	v703-v711	v712-v720	v722-v729

マスに1～9のいずれかの数字を入れる。
- aAは1～9のいずれかの数字を入れる
  - v1 v2 v3 v4 v5 v6 v7 v8 v9
  - v1,v2,v3,v4,v5,v6,v7,v8,v9の二つ以上は同時に真にならない
    以下、aA1～iI9をv数値に置き換えるだけなので割愛

ここまでのルールをCNFとして出力するjsのコードを用意しました。

let range = function*(s, e) {
  for (let i = s; i <= e; i++) {
    yield i;
  }
};

let index = (縦, 横, val) => val + 横 * 9 + 縦 * 9 * 9;

let cnf = [];

for (let clause of (function*() {
    // マスに1～9のいずれかの数字を入れる。
    for (let 縦 of range(0, 8)) {
      for (let 横 of range(0, 8)) {
        // aA1,aA2,aA3,aA4,aA5,aA6,aA7,aA8,aA9のいずれかは真である
        yield [...(function*(縦, 横) {
          for (let val of range(1, 9)) {
            yield index(縦, 横, val);
          }
        })(縦, 横)];
        // aA1,aA2,aA3,aA4,aA5,aA6,aA7,aA8,aA9の二つ以上は同時に真にならない
        for (let vala of range(1, 9 - 1)) {
          for (let valb of range(vala + 1, 9)) {
            yield [-index(縦, 横, vala), -index(縦, 横, valb)];
          }
        }
      }
    }

    for (let val of range(1, 9)) {
      // 横の各列に、同じ数字が重複して入ってはいけない。
      for (let 縦 of range(0, 8)) {
        for (let 横a of range(0, 8 - 1)) {
          for (let 横b of range(横a + 1, 8)) {
            yield [-index(縦, 横a, val), -index(縦, 横b, val)];
          }
        }
      }
      // 縦の各列に、同じ数字が重複して入ってはいけない。
      for (let 縦a of range(0, 8 - 1)) {
        for (let 縦b of range(縦a + 1, 8)) {
          for (let 横 of range(0, 8)) {
            yield [-index(縦a, 横, val), -index(縦b, 横, val)];
          }
        }
      }
      // 太線で囲まれた3×3のブロック内に、同じ数字が重複して入ってはいけない。
      for (let 縦ブロック of range(0, 2)) {
        for (let 横ブロック of range(0, 2)) {
          for (let 縦a of range(縦ブロック * 3, (縦ブロック + 1) * 3 - 1)) {
            for (let 横a of range(横ブロック * 3, (横ブロック + 1) * 3 - 1)) {
              for (let 横b of range(横a + 1, (横ブロック + 1) * 3 - 1)) {
                // 横の各列に～のルールで取り込み済みの為無くてもよい
                yield [-index(縦a, 横a, val), -index(縦a, 横b, val)];
              }
              for (let 縦c of range(縦a + 1, (縦ブロック + 1) * 3 - 1)) {
                for (let 横c of range(横ブロック * 3, (横ブロック + 1) * 3 - 1)) {
                  // 縦の各列に～のルールで取り込み済みの為横a==横cは無くてもよい
                  yield [-index(縦a, 横a, val), -index(縦c, 横c, val)];
                }
              }
            }
          }
        }
      }
    }
  })()) {
  cnf.push([...clause, 0].join(' '));
}

document.body.appendChild((() => {
  let e = document.createElement('div');
  e.innerText = 'p cnf ' + index(8, 8, 9) + ' ' + cnf.length;
  return e;
})());
for (let str of cnf) {
  document.body.appendChild((() => {
    let e = document.createElement('div');
    e.innerText = str;
    return e;
  })());
}

ここまででルール部分は定義できました。

あとは盤面の情報を追加します。
wikipediaの例を解く場合は
aA = 5
aB = 3
等が該当します。

aA5は真である
aB3は真である
aD7は真である
bA6は真である
bD1は真である
bE9は真である
bF5は真である
cB9は真である
cC8は真である
cH6は真である
dA8は真である
dE6は真である
dI3は真である
eA4は真である
eD8は真である
eF3は真である
eI1は真である
fA7は真である
fE2は真である
fI6は真である
gB6は真である
gG2は真である
gH8は真である
hD4は真である
hD4は真である
hE1は真である
hF9は真である
hI5は真である
iE8は真である
iH7は真である
iI9は真である

for (let clause of (function*() {
    // 中略
    yield [index(0, 0, 5)];
    yield [index(0, 1, 3)];
    yield [index(0, 4, 7)];
    yield [index(1, 0, 6)];
    yield [index(1, 3, 1)];
    yield [index(1, 4, 9)];
    yield [index(1, 5, 5)];
    yield [index(2, 1, 9)];
    yield [index(2, 2, 8)];
    yield [index(2, 7, 6)];
    yield [index(3, 0, 8)];
    yield [index(3, 4, 6)];
    yield [index(3, 8, 3)];
    yield [index(4, 0, 4)];
    yield [index(4, 3, 8)];
    yield [index(4, 5, 3)];
    yield [index(4, 8, 1)];
    yield [index(5, 0, 7)];
    yield [index(5, 4, 2)];
    yield [index(5, 8, 6)];
    yield [index(6, 1, 6)];
    yield [index(6, 6, 2)];
    yield [index(6, 7, 8)];
    yield [index(7, 3, 4)];
    yield [index(7, 4, 1)];
    yield [index(7, 5, 9)];
    yield [index(7, 8, 5)];
    yield [index(8, 4, 8)];
    yield [index(8, 7, 7)];
    yield [index(8, 8, 9)];
  })()) {
  cnf.push([...clause, 0].join(' '));
}

最終的なCNFは以下となりました。

先頭行の前半はCNF情報であることを示す固定文言
729は変数のMAX（今回だとiI9）
11775はルールの数
先頭行以外はルール。0は行末を表します。

p cnf 729 11775
1 2 3 4 5 6 7 8 9 0
-1 -2 0
-1 -3 0
Zennの80000文字制限に掛かった為全掲載は断念

組み立てたCNFでナンプレを解く

CNFをテキストファイルに保存して、minisatに流してみました。^[1]

SAT
-1 -2 -3 -4 5 -6 -7 -8 -9 -10 -11 12 -13 -14 -15 -16 -17 -18 -19 -20 -21 22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 33 -34 -35 -36 -37 -38 -39 -40 -41 -42 43 -44 -45 -46 -47 -48 -49 -50 -51 -52 53 -54 -55 -56 -57 -58 -59 -60 -61 -62 63 64 -65 -66 -67 -68 -69 -70 -71 -72 -73 74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 87 -88 -89 -90 -91 -92 -93 -94 -95 -96 97 -98 -99 -100 101 -102 -103 -104 -105 -106 -107 -108 109 -110 -111 -112 -113 -114 -115 -116 -117 -118 -119 -120 -121 -122 -123 -124 -125 126 -127 -128 -129 -130 131 -132 -133 -134 -135 -136 -137 138 -139 -140 -141 -142 -143 -144 -145 -146 -147 148 -149 -150 -151 -152 -153 -154 -155 -156 -157 -158 -159 -160 161 -162 163 -164 -165 -166 -167 -168 -169 -170 -171 -172 -173 -174 -175 -176 -177 -178 -179 180 -181 -182 -183 -184 -185 -186 -187 188 -189 -190 -191 192 -193 -194 -195 -196 -197 -198 -199 -200 -201 202 -203 -204 -205 -206 -207 -208 209 -210 -211 -212 -213 -214 -215 -216 -217 -218 -219 -220 221 -222 -223 -224 -225 -226 -227 -228 -229 -230 231 -232 -233 -234 -235 -236 -237 -238 -239 -240 241 -242 -243 -244 -245 -246 -247 -248 -249 -250 251 -252 -253 -254 -255 -256 257 -258 -259 -260 -261 -262 -263 -264 -265 -266 -267 -268 -269 270 -271 -272 -273 -274 -275 -276 277 -278 -279 -280 -281 -282 -283 -284 285 -286 -287 -288 289 -290 -291 -292 -293 -294 -295 -296 -297 -298 -299 -300 301 -302 -303 -304 -305 -306 -307 308 -309 -310 -311 -312 -313 -314 -315 -316 -317 318 -319 -320 -321 -322 -323 -324 -325 -326 -327 328 -329 -330 -331 -332 -333 -334 335 -336 -337 -338 -339 -340 -341 -342 -343 -344 -345 -346 -347 348 -349 -350 -351 -352 -353 -354 -355 -356 -357 -358 359 -360 -361 -362 -363 -364 365 -366 -367 -368 -369 -370 -371 372 -373 -374 -375 -376 -377 -378 -379 -380 -381 -382 -383 -384 385 -386 -387 -388 -389 -390 -391 -392 -393 -394 -395 396 397 -398 -399 -400 -401 -402 -403 -404 -405 -406 -407 -408 -409 -410 -411 412 -413 -414 415 -416 -417 -418 -419 -420 -421 -422 -423 -424 -425 426 -427 -428 -429 -430 -431 -432 -433 -434 -435 -436 -437 -438 -439 -440 441 -442 443 -444 -445 -446 -447 -448 -449 -450 -451 -452 -453 454 -455 -456 -457 -458 -459 -460 -461 -462 -463 -464 -465 -466 467 -468 -469 -470 -471 -472 473 -474 -475 -476 -477 -478 -479 -480 -481 -482 483 -484 -485 -486 -487 -488 -489 -490 -491 -492 -493 -494 495 -496 -497 -498 -499 -500 501 -502 -503 -504 505 -506 -507 -508 -509 -510 -511 -512 -513 -514 -515 -516 -517 518 -519 -520 -521 -522 -523 -524 525 -526 -527 -528 -529 -530 -531 -532 -533 -534 -535 -536 -537 538 -539 -540 -541 542 -543 -544 -545 -546 -547 -548 -549 -550 -551 -552 -553 -554 -555 -556 557 -558 -559 -560 -561 562 -563 -564 -565 -566 -567 -568 569 -570 -571 -572 -573 -574 -575 -576 -577 -578 -579 -580 -581 -582 -583 584 -585 -586 -587 -588 -589 -590 -591 592 -593 -594 -595 -596 -597 598 -599 -600 -601 -602 -603 604 -605 -606 -607 -608 -609 -610 -611 -612 -613 -614 -615 -616 -617 -618 -619 -620 621 -622 -623 -624 -625 -626 627 -628 -629 -630 -631 -632 633 -634 -635 -636 -637 -638 -639 -640 -641 -642 -643 644 -645 -646 -647 -648 -649 -650 651 -652 -653 -654 -655 -656 -657 -658 -659 -660 661 -662 -663 -664 -665 -666 -667 -668 -669 -670 671 -672 -673 -674 -675 -676 677 -678 -679 -680 -681 -682 -683 -684 -685 -686 -687 -688 -689 -690 -691 692 -693 -694 -695 -696 -697 -698 699 -700 -701 -702 703 -704 -705 -706 -707 -708 -709 -710 -711 -712 -713 -714 -715 -716 -717 718 -719 -720 -721 -722 -723 -724 -725 -726 -727 -728 729 0

否定を表す「-」を無視すると

SAT
 5 12 22 33 43 53 63 64 74 87 97 101 109 126 131 138 148 161 163 180 188 192 202 209 221 231 241 251 257 270 277 285 289 301 308 318 328 335 348 359 365 372 385 396 397 412 415 426 441 443 454 467 473 483 495 501 505 518 525 538 542 557 562 569 584 592 598 604 621 627 633 644 651 661 671 677 692 699 703 718 729 0

マス目が9x9で81個に対して、0以外の数が81個出力されたのでとりあえず個数が一致していることがわかります。

これらの数字は上記の話をした中のvNに相当するものなので、aAの形に逆変換してみます。

0: (3) [5, 'aA', 5]
1: (3) [12, 'aB', 3]
2: (3) [22, 'aC', 4]
3: (3) [33, 'aD', 6]
4: (3) [43, 'aE', 7]
5: (3) [53, 'aF', 8]
6: (3) [63, 'aG', 9]
7: (3) [64, 'aH', 1]
8: (3) [74, 'aI', 2]
9: (3) [87, 'bA', 6]
10: (3) [97, 'bB', 7]
11: (3) [101, 'bC', 2]
12: (3) [109, 'bD', 1]
13: (3) [126, 'bE', 9]
14: (3) [131, 'bF', 5]
15: (3) [138, 'bG', 3]
16: (3) [148, 'bH', 4]
17: (3) [161, 'bI', 8]
18: (3) [163, 'cA', 1]
19: (3) [180, 'cB', 9]
20: (3) [188, 'cC', 8]
21: (3) [192, 'cD', 3]
22: (3) [202, 'cE', 4]
23: (3) [209, 'cF', 2]
24: (3) [221, 'cG', 5]
25: (3) [231, 'cH', 6]
26: (3) [241, 'cI', 7]
27: (3) [251, 'dA', 8]
28: (3) [257, 'dB', 5]
29: (3) [270, 'dC', 9]
30: (3) [277, 'dD', 7]
31: (3) [285, 'dE', 6]
32: (3) [289, 'dF', 1]
33: (3) [301, 'dG', 4]
34: (3) [308, 'dH', 2]
35: (3) [318, 'dI', 3]
36: (3) [328, 'eA', 4]
37: (3) [335, 'eB', 2]
38: (3) [348, 'eC', 6]
39: (3) [359, 'eD', 8]
40: (3) [365, 'eE', 5]
41: (3) [372, 'eF', 3]
42: (3) [385, 'eG', 7]
43: (3) [396, 'eH', 9]
44: (3) [397, 'eI', 1]
45: (3) [412, 'fA', 7]
46: (3) [415, 'fB', 1]
47: (3) [426, 'fC', 3]
48: (3) [441, 'fD', 9]
49: (3) [443, 'fE', 2]
50: (3) [454, 'fF', 4]
51: (3) [467, 'fG', 8]
52: (3) [473, 'fH', 5]
53: (3) [483, 'fI', 6]
54: (3) [495, 'gA', 9]
55: (3) [501, 'gB', 6]
56: (3) [505, 'gC', 1]
57: (3) [518, 'gD', 5]
58: (3) [525, 'gE', 3]
59: (3) [538, 'gF', 7]
60: (3) [542, 'gG', 2]
61: (3) [557, 'gH', 8]
62: (3) [562, 'gI', 4]
63: (3) [569, 'hA', 2]
64: (3) [584, 'hB', 8]
65: (3) [592, 'hC', 7]
66: (3) [598, 'hD', 4]
67: (3) [604, 'hE', 1]
68: (3) [621, 'hF', 9]
69: (3) [627, 'hG', 6]
70: (3) [633, 'hH', 3]
71: (3) [644, 'hI', 5]
72: (3) [651, 'iA', 3]
73: (3) [661, 'iB', 4]
74: (3) [671, 'iC', 5]
75: (3) [677, 'iD', 2]
76: (3) [692, 'iE', 8]
77: (3) [699, 'iF', 6]
78: (3) [703, 'iG', 1]
79: (3) [718, 'iH', 7]
80: (3) [729, 'iI', 9]

全てのマスに一つずつ入ってることがこの時点でもわかりますね。

表に入れてみます。

	A	B	C	D	E	F	G	H	I
a	5	3	4	6	7	8	9	1	2
b	6	7	2	1	9	5	3	4	8
c	1	9	8	3	4	2	5	6	7
d	8	5	9	7	6	1	4	2	3
e	4	2	6	8	5	3	7	9	1
f	7	1	3	9	2	4	8	5	6
g	9	6	1	5	3	7	2	8	4
h	2	8	7	4	1	9	6	3	5
i	3	4	5	2	8	6	1	7	9

合ってる！

まとめ

CNFは一行が論理和、行間が論理積、マイナス記号が否定を表すよ
CNFは変数名を自由につけることはできないよ、だから自分で何番目の変数が何だったか覚えておく必要があるよ、あと扱えるのは真偽値のみですよ

お疲れさまでした。

脚注

DockerのDebianイメージで「apt-get update && apt-get install -y minisat2」したものを使用しました。CNFの作り方が主題の為割愛 ↩︎

	A	B	C	D	E	F	G	H	I
a	aA	aB	aC	aD	aE	aF	aG	aH	aI
b	bA	bB	bC	bD	bE	bF	bG	bH	bI
c	cA	cB	cC	cD	cE	cF	cG	cH	cI
d	dA	dB	dC	dD	dE	dF	dG	dH	dI
e	eA	eB	eC	eD	eE	eF	eG	eH	eI
f	fA	fB	fC	fD	fE	fF	fG	fH	fI
g	gA	gB	gC	gD	gE	gF	gG	gH	gI
h	hA	hB	hC	hD	hE	hF	hG	hH	hI
i	iA	iB	iC	iD	iE	iF	iG	iH	iI

	A	B	C	D	E	F	G	H	I
a	5	3	4	6	7	8	9	1	2
b	6	7	2	1	9	5	3	4	8
c	1	9	8	3	4	2	5	6	7
d	8	5	9	7	6	1	4	2	3
e	4	2	6	8	5	3	7	9	1
f	7	1	3	9	2	4	8	5	6
g	9	6	1	5	3	7	2	8	4
h	2	8	7	4	1	9	6	3	5
i	3	4	5	2	8	6	1	7	9

	A	B	C	D	E	F	G	H	I
a	aA	aB	aC	aD	aE	aF	aG	aH	aI
b	bA	bB	bC	bD	bE	bF	bG	bH	bI
c	cA	cB	cC	cD	cE	cF	cG	cH	cI
d	dA	dB	dC	dD	dE	dF	dG	dH	dI
e	eA	eB	eC	eD	eE	eF	eG	eH	eI
f	fA	fB	fC	fD	fE	fF	fG	fH	fI
g	gA	gB	gC	gD	gE	gF	gG	gH	gI
h	hA	hB	hC	hD	hE	hF	hG	hH	hI
i	iA	iB	iC	iD	iE	iF	iG	iH	iI

	A	B	C	D	E	F	G	H	I
a	5	3	4	6	7	8	9	1	2
b	6	7	2	1	9	5	3	4	8
c	1	9	8	3	4	2	5	6	7
d	8	5	9	7	6	1	4	2	3
e	4	2	6	8	5	3	7	9	1
f	7	1	3	9	2	4	8	5	6
g	9	6	1	5	3	7	2	8	4
h	2	8	7	4	1	9	6	3	5
i	3	4	5	2	8	6	1	7	9

そもそもCNFって何だっけ？

ナンプレを解くCNFを組み立てる

組み立てたCNFでナンプレを解く

まとめ

Discussion

	A	B	C	D	E	F	G	H	I
a	aA	aB	aC	aD	aE	aF	aG	aH	aI
b	bA	bB	bC	bD	bE	bF	bG	bH	bI
c	cA	cB	cC	cD	cE	cF	cG	cH	cI
d	dA	dB	dC	dD	dE	dF	dG	dH	dI
e	eA	eB	eC	eD	eE	eF	eG	eH	eI
f	fA	fB	fC	fD	fE	fF	fG	fH	fI
g	gA	gB	gC	gD	gE	gF	gG	gH	gI
h	hA	hB	hC	hD	hE	hF	hG	hH	hI
i	iA	iB	iC	iD	iE	iF	iG	iH	iI

	A	B	C	D	E	F	G	H	I
a	5	3	4	6	7	8	9	1	2
b	6	7	2	1	9	5	3	4	8
c	1	9	8	3	4	2	5	6	7
d	8	5	9	7	6	1	4	2	3
e	4	2	6	8	5	3	7	9	1
f	7	1	3	9	2	4	8	5	6
g	9	6	1	5	3	7	2	8	4
h	2	8	7	4	1	9	6	3	5
i	3	4	5	2	8	6	1	7	9