0

次の定義を前提としています。

type Index = Int

data BExp = Prim Bool | IdRef Index | Not BExp | And BExp BExp | Or BExp BExp
           deriving (Eq, Ord, Show)

type NodeId = Int

type BDDNode =  (NodeId, (Index, NodeId, NodeId))

type BDD = (NodeId, [BDDNode])

ブール式からROBDDを構築したい。これまでのところ、非冗長性または共有性を満たさない BDD を構築できました。

buildBDD :: BExp -> [Index] -> BDD
buildBDD e idxs
 = buildBDD' e 2 idxs

buildBDD' :: BExp -> NodeId -> [Index] -> BDD
buildBDD' (Prim bool) _ []
  | bool       = (1, [])
  | otherwise  = (0, [])
buildBDD' e nodeId (idx : idxs)
 = (nodeId, [newNode] ++ tl ++ tr)
 where
   newNode = (nodeId, (idx, il, ir))
   (il, tl) = buildBDD' (restrict e idx False) (2 * nodeId) idxs
   (ir, tr) = buildBDD' (restrict e idx True) (2 * nodeId + 1) idxs

これはまだ進行中の作業であるため、ネーミングとスタイルは最適ではない可能性があります。

ノードは、一意の ID によって内部的に表されます。2 から始まります。左側のサブツリーのルート ノードには2nというラベルが付けられ、右側のサブツリーのルート ノードには2n + 1というラベルが付けられます。

この関数は、ブール式と、式に現れる変数のインデックスのリストを入力として受け取ります。

たとえば、次の式の場合:

And (IdRef 7) (Or (IdRef 2) (Not (IdRef 3)))

コールbuildBDD bexp [2,3,7]が返ってきます

(2,[(2,(2,4,5)),(4,(3,8,9)),(8,(7,0,1)),(9,(7,0,0)),(5,(3,10,11)),(10,(7,0,1)),
(11,(7,0,1))])

冗長性のないプロパティを考慮して、次の変更を加えました(これは完全にはテストされていませんが、機能しているようです)。

checkEqual (_, l, r)
  | l == r    = True
  | otherwise = False

getElemFromTuple (_, _, e)
  = e

getTuple = snd . head

buildROBDD' e nodeId (idx : idxs)
     = (nodeId, [newNode] ++ left ++ right)
 where
   newNode   = (nodeId, (idx, lId, rId))
   (il, tl)  = buildROBDD' (restrict e idx False) (2 * nodeId) idxs
   (ir, tr)  = buildROBDD' (restrict e idx True) (2 * nodeId + 1) idxs
   lId       = if (not . null) tl && (checkEqual . getTuple) tl then (getElemFromTuple . getTuple) tl else il
   rId       = if (not . null) tr && (checkEqual . getTuple) tr then (getElemFromTuple . getTuple) tr else ir
   left      = if (not . null) tl && (checkEqual . getTuple) tl then [] else tl
   right     = if (not . null) tr && (checkEqual . getTuple) tr then [] else tr

(上記の不自然な表現をお許しください)

ただし、特に共有ノードがグラフのどこかにある可能性があり、現在のツリーを保存していないため、共有プロパティにアプローチする方法がわかりません。一意のノード ID の式は、必要に応じて変更できます。

注: これは練習用であるため、関連する型とスタイルは最適ではない可能性があります。また、それらを変更することも想定されていません（機能を自由に変更できます）。

4

0 に答える 0