决策图不再数子函数:改用割矩阵的秩,ATDD在任意vtree上给出唯一规范形
树决策图(TDD)按每个vtree割上不同子函数的个数计宽,这种计数看不见子函数之间的线性相关。把计数换成割矩阵的秩,得到代数树决策图(ATDD),其宽度即因子秩,且对每个函数和每个vtree只有唯一表示。ATDD比TDD指数级更简洁,比结构化确定性DNNF准多项式更简洁,同时保留多项式时间的模型计数、加权模型计数与等价检查。
树决策图(TDD)按每个vtree割上不同子函数的个数计宽,这种计数看不见子函数之间的线性相关。把计数换成割矩阵的秩,得到代数树决策图(ATDD),其宽度即因子秩,且对每个函数和每个vtree只有唯一表示。ATDD比TDD指数级更简洁,比结构化确定性DNNF准多项式更简洁,同时保留多项式时间的模型计数、加权模型计数与等价检查。
已读完全部报道