2010-07-18 [長年日記]
λ. IDPで 3 not problem を解けなかった
以前に
- 3 not problem - ヒビルテ(2008-07-16)
- Alloy で 3 not problem を解く - ヒビルテ(2008-07-16)
- Otter で 3 not problem を解く - ヒビルテ(2008-07-18)
辺りで書いた 3 not problem (別名: The 2-inverter puzzle) を、IDP (Inductive Definition Programming) で解いてみようとした。 が、うまくいかなかったという話。
回路の構成自体を解として直接求めるのは、Alloyや他のソルバーでうまくいってなかったので、Otterの場合と同じく、notを使う箇所だけを解として求めることにした。 具体的には「notを適用する真理値表Inv1,Inv2が与えられた時に真理値表xsが計算可能である」ことを表す述語P(xs)を帰納的に定義して、出力となる真理値表がこの述語を満たすときのInv1,Inv2の値を解として求める。 一階述語論理の普通のモデル発見器では帰納的な定義ができないので、こういうやり方を出来るのは、IDPとかASPくらいのはず。
定式化自体は two_inv.idp.gz のように非常に簡単にできた。ただ、ビット演算のやり方が分からないので、そこは定数とテーブルを自前で用意することで対処した。その辺りのつまらない部分を省略したものを以下に示す。
Given:
type BV8 = {
B00000000;
B00000001;
〜(中略)〜
B11111111;
}
BIT_NOT (BV8) : BV8
BIT_AND (BV8,BV8) : BV8
BIT_OR (BV8,BV8) : BV8
Find:
Inv1 : BV8
Inv2 : BV8
Declare:
P (BV8)
Satisfying:
{ P(B00001111). // input 1
P(B00110011). // input 2
P(B01010101). // input 3
P(BIT_AND(x,y)) <- P(x) & P(y).
P(BIT_OR(x,y)) <- P(x) & P(y).
P(BIT_NOT(Inv1)) <- P(Inv1).
P(BIT_NOT(Inv2)) <- P(Inv2).
}
P(B11110000). // output 1
P(B11001100). // output 2
P(B10101010). // output 3
Data:
BIT_NOT = {
B00000000 -> B11111111;
〜(中略)〜
B11111111 -> B00000000;
}
BIT_AND = {
B00000000,B00000000 -> B00000000;
B00000000,B00000001 -> B00000000;
〜(中略)〜
B11111111,B11111111 -> B11111111;
}
BIT_OR = {
B00000000,B00000000 -> B00000000;
B00000000,B00000001 -> B00000001;
〜(中略)〜
B11111111,B11111111 -> B11111111;
}
だけど、実際に gidl.exe two_inv.idp | midl.exe と実行してみたら、midl.exe が「This application has requested the Runtime to terminate it in an unusual way. Please contact the application's support team for more information.」で落ちた。残念。
関連
λ. ASPで 3 not problem を解いた
IDP (Inductive Definition Programming) でダメなら、解集合プログラミング(Answer Set Programming, ASP)でということで、やってみた。 ソルバには例によって、Potasscoで配布されているclingoを利用。入力は以下のようにした(two_inv.lp)。IDPの場合と違って、ASPの場合はプログラム全体が帰納的定義になっていて、欲しい結果がpに含まれない場合を一貫性制約(integrity constraint)を使って弾いている。
% domain predicate
bv8(0..255).
% inv(X)を満たすbv8(X)はたかだか2つ
0{inv(X) : bv8(X)}2.
p(15). % input 1 (15 = 0b00001111)
p(51). % input 2 (51 = 0b00110011)
p(85). % input 3 (85 = 0b01010101)
p(X & Y) :- p(X), p(Y), bv8(X), bv8(Y).
p(X ? Y) :- p(X), p(Y), bv8(X), bv8(Y).
p(~X & 255) :- p(X), inv(X), bv8(X).
% integrity constraint
:- not p(240). % output 1 (240 = 0b11110000)
:- not p(204). % output 2 (204 = 0b11001100)
:- not p(170). % output 3 (170 = 0b10101010)
これを clingo-2.0.3-win32.exe -n 0 two_inv.lp として実行した結果が two_inv_asp.txt 。オプションの -n 0 はモデルを全て列挙するという指定で、出力から inv(23), inv(105) なるモデルが唯一のモデルであることがわかる。
このnotを使う箇所は当然ながらOtterが見つけたものと同じものになっている。
このモデルから直接分かるのは、2つのnotを使う箇所だけだけど、ここから回路全体を構成するのは難しくない。
ASPすごいな、と初めて思ったよ。
関連
λ. 何故ASPがすごいと思ったか補足
なんでASPがすごいかと思ったかというと、Pが帰納的(最小)であるという制約を除いたものを、有名なSMTソルバーであるYices(1.0.28)とCVC3(2010-07-11)に食わせてみて、ぜんぜん答えが出なかったので。
