日々の流転

λ. お菓子買いだめ

あまり沢山買ったつもりはなかったけど、予算オーバー。

λ. 3 not problem

x,y,zの3入力, x',y',z'の3出力を持つブラックボックスがある. 入出力の関係は

• x' = not x
• y' = not y
• z' = not z

である. ブラックボックスには, andとorは好きなだけ使われているが, notは2つしかないことが分かっている. 内部はどうなっているか.

ささださんのだいありー(2008-07-15)と、 3 not の問題 - まめめも(2008-07-16)経由で。 例によってAlloyで解こうとしたら、Alloy Analyer のバグを踏んだっぽい(追記: どうもバグではなく仕様だったっぽい)。 あと、昔Otter関係で聞いたことのある話だなと思ったら、<URL:http://www-unix.mcs.anl.gov/AR/otter/examples33/program/two_inv.in> にあった。

λ. Alloy で 3 not problem を解く

以下のような感じで書いたのだけど、Alloy Analyzer にかけたところ、残念ながら数時間程度では解けない感じだった。Otterでやっているように、真理値表を8bit整数で表してビットごとのandやorで操作できると、もうちょっと効率よくなりそうなんだけど、今のAlloyにはそれらのビット演算はないのだった。ビットシフトはあるのに……(涙

/*
The 2-inverter puzzle.

The problem is to build a combinational circuit with 3 inputs
and 3 outputs, such that the outputs negate the inputs; we can
use as many AND and OR gates as we wish, but at most 2 NOT gates.
*/

abstract sig Bool {}
one sig True, False extends Bool {}

abstract sig Node {
   t : set (Bool -> Bool -> Bool)
}
sig Not extends Node {
   i : Node
}
abstract sig Op2 extends Node {
   i1 : Node,
   i2 : Node,
}
sig And, Or extends Op2 {}
one sig X,Y,Z extends Node {}

pred v[n : Node, a : Bool, b : Bool, c : Bool] {
   (a->b->c) in n.t
}

fact {
   no n : Node | n in n.^(i + i1 + i2)
   all a,b,c : Bool {
      v[X,a,b,c] <=> (a=True)
      v[Y,a,b,c] <=> (b=True)
      v[Z,a,b,c] <=> (c=True)
      all n : Not | v[n,a,b,c] <=> !v[n.i,a,b,c]
      all n : And | v[n,a,b,c] <=> (v[n.i1,a,b,c] && v[n.i2,a,b,c])
      all n : Or  | v[n,a,b,c] <=> (v[n.i1,a,b,c] || v[n.i2,a,b,c])
   }
}

pred show() {}
run show for 10

pred two_inv {
   some n1,n2,n3 : Node {
      all a,b,c : Bool {
         v[n1,a,b,c] <=> !v[X,a,b,c]
         v[n2,a,b,c] <=> !v[Y,a,b,c]
         v[n3,a,b,c] <=> !v[Z,a,b,c]
      }
   }
}
run two_inv for 25 Node, exactly 2 Not