ACPC Day1 D - Darseinのプロコン日記

会津合宿Day1のD問題に「与えられた真理値表に対応するBDDを構築し、頂点数を求めよ」という問題が出ました。
想定解法は「二分決定木作って頑張って簡約化」らしいですが、これはBDDを構築しなくても解けます。

変数をx1,x2,...,xn、与えられた真理値表を表す文字列をsとします。

ここで、sの前半2^(n-1)個はx1を0に固定したとき、後半2^(n-1)個はx1を1に固定したときの真理値表を表していることに注目します。
これをBDD上で考えると、変数がx1のノードで、前半が左の子、後半が右の子に対応する部分BDDを表している、と考えることができます。
ということはまず、前半と後半が一致する場合は、左のエッジも右のエッジも同じ部分BDDを指している、すなわち、冗長なノードの削除ルールに当てはまるため、前半が表すBDDの頂点数だけが分かれば良いことになります。

また、この長さ2^(n-1)の01文字列がそれぞれ部分BDDである、という発想から逆に、同じ01文字列であれば、同じBDDを表している、と見ることが出来ます。
よって、今までに現れたことがある長さ2^xの01文字列であれば、それはすでに調べた部分BDDであるので、数を数える必要はありません。これは等価なノードの共有にあたります。

ということで、結論としては、与えられた文字列をどんどん半分に区切っていく過程で現れた文字列の中で、その文字列の前半と後半が一致しないような文字列の種類数がBDDサイズに等しい、ということになります。

この、

長さ2^nの2進文字列
前半と後半が一致しない

を満たす文字列はBeadsと呼ばれ、BDDと一対一対応したハッシュ関数のようなものとして機能することがKnuthのThe Art of Computer Programming 4-1で述べられています。
BDDサイズの上界を見積もるのにも用いられていたと記憶しています。

D問題に対するACコード例は、以下の通りです。

#include<iostream>
#include<string>
#include<set>
using namespace std;

set<string> hash;

int parse(string s){
  if(s.size()==1)return 0;
  if(hash.find(s) != hash.end())return 0;

  string a = s.substr(0,s.size()/2), b = s.substr(s.size()/2);
  int res;
  if(a==b)res = parse(a);
  else res = parse(a) + parse(b) + 1;

  hash.insert(s);
  return res;
}

int main(){
  int n;
  string s;
  cin >> n >> s;
  cout << parse(s) << endl;
}