蕴含图的构建与搜索

标签：eve   搜索   trail   进入   使用   查询   nbsp   赋值   --   

思考：

1.主要为了基于冲突往前搜索，所以关注冲突节点。冲突是两个子句对一个文字赋值给出不同的赋值产生的，因而冲突节点实际关联两个子句。

冲突文字——关联两个reason子句，两个决策层；

普通决策（含隐含决策）文字——关联一个reason子句，一个决策层；

2.使用有向图建立蕴含图：

（1）顶点为进入trail的文字：

trail.push_(p);//文字入队

以下循环可以查询指定队列位置号上的文字及其变元

for (int c = trail.size() - 1; c >= trailRecord; c--)
{
      Var x = var(trail[c]);
     assigns[x] = l_Undef;

}

assigns[var(p)]              ——可获取其变元赋值
vardata[var(p)].reason ——可获取获取其所在的子句地址

vardata[var(p)].level    ——可获取其所在的决策层数

由上边查询及访问可知指导trail的位置序号——可以得到文字——进而通过变元获取其它对应信息。所以构建

指向关系逻辑上是a->b，a先赋值后蕴含推导出b，a在前由指向b；实际便于查找可以建立有向边b指向a。

蕴含图的构建与搜索

标签：eve   搜索   trail   进入   使用   查询   nbsp   赋值   --   

原文地址：https://www.cnblogs.com/yuweng1689/p/12730847.html