两种基于Tableaux算法的reasoner的源码分析（1）
最近更新：2026-07-16   |   字数总计：1.6k   |   阅读估时：6分钟   |   阅读量：次
  1. 两种基于Tableaux算法的reasoner的源码分析（1）
    1. 一、两种reasoner的简单介绍
      1. FaCT++
    2. 二、项目结构概览
    3. 三、Reasoner.h —— 核心架构解析
      1. 3.1 头文件引用分析
      2. 3.2 这个文件在FaCT++中的角色
      3. 3.3 核心数据结构
      4. 3.4 规则处理函数（Tactics）
    4. 四、Reasoner.cpp —— 核心流程实现
      1. 4.1 外部入口：runSat
      2. 4.2 私有 runSat() → checkSatisfiability()
      3. 4.3 commonTactic() → 分发到具体 Tactic
    5. 五、核心流程总结
    6. 六、关键设计亮点

两种基于Tableaux算法的reasoner的源码分析（1）

一、两种reasoner的简单介绍

FaCT++

FaCT++是一个基于Tableaux的推理器，用于表达描述逻辑 (DL)。它涵盖了 OWL 和 OWL 2（缺乏对关键约束和某些数据类型的支持）基于 DL 的本体语言。它可以用作独立的 DIG 推理器，或用作基于 OWL API 的应用程序的后端推理器。现在它被用作 Protege 4 OWL 编辑器中的默认推理器之一。

FaCT++ 最初是与 Ian Horrocks 在 WonderWeb 项目中一起开发的。

资源链接：https://drive.google.com/drive/folders/0B688Ilel_jz_OVktYU5SdGpsek0?resourcekey=0-eyXKhUPahgv6JW74aLy5bw

源码仓库：https://bitbucket.org/dtsarkov/factplusplus/src/master/

二、项目结构概览

项目结构概览

在分析源码之前，我们先找到两个核心文件：

  • reasoner.h：推理机的头文件，定义核心类与接口
  • reasoner.cpp：推理机的实现文件，包含Tableau算法的具体逻辑

三、Reasoner.h —— 核心架构解析

3.1 头文件引用分析

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
#ifndef REASONER_H
#define REASONER_H

#include "globaldef.h"
#include "tBranchingContext.h"
#include "dlCompletionGraph.h"
#include "dlTBox.h"
#include "dlDag.h"
#include "modelCacheIan.h"
#include "tSaveStack.h"
#include "procTimer.h"
#include "DataReasoning.h"
#include "ToDoList.h"
#include "tFastSet.h"

#if USE_LOGGING
#   define USE_REASONING_STATISTICS
#endif

通过引用可以看出FaCT++的模块化架构：

头文件 作用
globaldef.h 全局定义与常量
tBranchingContext.h 分支上下文（处理非确定性）
dlCompletionGraph.h 完成图（Completion Graph）管理
dlTBox.h TBox（术语公理）定义
dlDag.h DAG（共享概念表达式）
modelCacheIan.h 模型缓存（优化）
tSaveStack.h 保存/恢复栈（回溯）
DataReasoning.h 数据类型推理
ToDoList.h 任务优先级队列
tFastSet.h 快速集合（用于已用概念追踪）

3.2 这个文件在FaCT++中的角色

Reasoner.h 定义了 DlSatTester 类，这个类是 Tableau 算法的实际执行引擎：

  • 它是推理的"大脑"：所有关于"如何判断一个概念是否可满足"的逻辑都在这里
  • 它与TBox紧密协作：通过 TBox& tBox 获取公理、角色、DAG
  • 它管理推理过程：维护 Completion Graph（CGraph）、ToDo List（TODO）、分支栈（Stack）、缓存等

你可以把它看作一个 “状态机 + 规则引擎”。

3.3 核心数据结构

成员 类型 作用
CGraph DlCompletionGraph 当前正在构造的模型（节点=个体，边=角色关系）
TODO ToDoList 优先级队列，存储待处理的概念表达式（Tableau的"任务列表"）
Stack BCStack 分支上下文栈，用于回溯（处理 ⊔ 等非确定性规则）
curNode DlCompletionTree* 当前正在处理的节点
curConcept ConceptWDep 当前正在处理的概念（含依赖集）
clashSet DepSet 冲突的依赖集（用于回溯）

3.4 规则处理函数（Tactics）

这些是 Tableau 扩展规则的直接实现，命名直观：

函数 对应规则 说明
commonTacticBodyId 原子概念 通常直接返回，不做扩展
commonTacticBodyAnd ⊓-规则（合取） 拆开合取，将两个子概念加入 TODO
commonTacticBodyOr ⊔-规则（析取） 非确定性分支，创建分支上下文
commonTacticBodySome ∃-规则（存在） 创建新个体，添加边和概念
commonTacticBodyAll ∀-规则（全称） 对每个现有邻居传播全称限制
commonTacticBodyGE ≥-规则（至少限制） 生成 n 个不同邻居
commonTacticBodyLE ≤-规则（至多限制） 合并多余的邻居
commonTacticBodyFunc 功能限制 处理 ≤1 R（特殊优化）
commonTacticBodyNN NN-规则 处理名义（Nominal）节点
commonTacticBodyChoose Choose-规则 处理 ⊔ 在数量限制中的特殊优化

四、Reasoner.cpp —— 核心流程实现

4.1 外部入口：runSat

1
2
3
4
5
6
7
8
9
10
11
12
bool runSat ( BipolarPointer p, BipolarPointer q = bpTOP )
{
    prepareReasoner();
    if ( initNewNode ( CGraph.getRoot(), DepSet(), p ) ||
         addToDoEntry ( CGraph.getRoot(), ConceptWDep(q) ) )
        return false;        // 初始就冲突
    TsProcTimer& timer = q == bpTOP ? satTimer : subTimer;
    timer.Start();
    bool result = runSat();  // 私有方法，执行实际推理
    timer.Stop();
    return result;
}

流程说明：

  1. prepareReasoner()：重置推理状态
  2. initNewNode：创建根节点并添加初始概念 p
  3. addToDoEntry：若 q 存在，添加第二个概念（用于子sumption测试）
  4. 调用私有 runSat() 进入主循环
  5. 返回推理结果

4.2 私有 runSat() → checkSatisfiability()

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
bool checkSatisfiability ( void )
{
    while ( !TODO.empty() )
    {
        // 取出最高优先级的待处理条目
        TODO.getNext ( curNode, curConcept );
        if ( isIBlocked() ) continue;  // 如果节点被阻塞，跳过
        if ( commonTactic() )          // 执行对应的规则
        {
            // 如果返回 true，表示产生冲突，需要回溯
            if ( tunedRestore() )
                return false;          // 无法恢复 -> 不可满足
            // 否则继续循环
        }
    }
    return performAfterReasoning();    // 所有规则处理完，检查最终状态
}

关键点：

  • TODO.getNext 使用优先级队列选择下一个要处理的概念（这是 FaCT++ 的关键优化）
  • commonTactic() 根据概念类型分发到具体的 Tactic 函数
  • 若 Tactic 返回 true（冲突），则调用 tunedRestore() 尝试回溯到最近的分支点

4.3 commonTactic() → 分发到具体 Tactic

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
bool commonTactic ( void )
{
    incStat(nTacticCalls);
    logStartEntry();
    const DLVertex& cur = DLHeap[curConcept.bp()];
    bool res = commonTacticBody(cur);
    logFinishEntry(res);
    return res;
}

bool commonTacticBody ( const DLVertex& cur )
{
    switch ( cur.Type() )
    {
        case dtTop:          return false;
        case dtBottom:       return addToDoEntry ( curNode, bpBOTTOM, ... );
        case dtAnd:          return commonTacticBodyAnd(cur);
        case dtOr:           return commonTacticBodyOr(cur);
        case dtForall:       return commonTacticBodyAll(cur);
        case dtExists:       return commonTacticBodySome(cur);
        case dtLE:           return commonTacticBodyLE(cur);
        case dtGE:           return commonTacticBodyGE(cur);
        case dtFunc:         return commonTacticBodyFunc(cur);
        // ... 其他类型
    }
}

分发逻辑：

  • 根据当前概念的类型（cur.Type()）选择对应的处理函数
  • 每种类型对应一个 Tableau 扩展规则
  • 这种设计模式类似于策略模式（Strategy Pattern），使规则易于扩展和维护

五、核心流程总结

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
┌─────────────────────────────────────────────────────────────┐
│                      runSat (外部入口)                       │
│  1. prepareReasoner() 重置状态                              │
│  2. initNewNode() 创建根节点 + 添加概念 p                    │
│  3. addToDoEntry() 添加概念 q（可选）                        │
└─────────────────────────┬───────────────────────────────────┘
                          ▼
┌─────────────────────────────────────────────────────────────┐
│              runSat() → checkSatisfiability()                │
│  while ( TODO 非空 ) {                                      │
│      TODO.getNext() 取出最高优先级任务                      │
│      if ( isIBlocked() ) continue;    ← 阻塞检查            │
│      if ( commonTactic() ) {           ← 执行规则            │
│          if ( tunedRestore() )         ← 回溯                │
│              return false;             ← 不可满足            │
│      }                                                       │
│  }                                                           │
└─────────────────────────┬───────────────────────────────────┘
                          ▼
┌─────────────────────────────────────────────────────────────┐
│                  commonTactic() 规则分发                    │
│  switch ( cur.Type() ) {                                    │
│      dtAnd:    commonTacticBodyAnd()   ← ⊓-规则             │
│      dtOr:     commonTacticBodyOr()    ← ⊔-规则（分支）     │
│      dtExists: commonTacticBodySome()  ← ∃-规则（创建节点） │
│      dtForall: commonTacticBodyAll()   ← ∀-规则（传播）     │
│      dtLE:     commonTacticBodyLE()    ← ≤-规则（合并）     │
│      dtGE:     commonTacticBodyGE()    ← ≥-规则（生成）     │
│  }                                                           │
└─────────────────────────────────────────────────────────────┘

六、关键设计亮点

设计亮点 说明
TODO优先级队列 区别于标准Tableau的深度优先，通过优先级调度提升搜索效率
规则策略模式 通过 commonTacticBody 分发，每种规则独立实现，易于扩展
阻塞机制 isIBlocked() 检查确保算法在循环定义下终止
依赖集回溯 冲突时仅回溯到相关分支点，而非完全重置
缓存优化 模型缓存加速包含关系测试

AI参与声明：本文档在撰写过程中使用了AI辅助工具进行内容整理、格式优化与润色。所有核心概念与代码分析均基于FaCT++源码与公开学术文献，并经人工校验与补充。


上一篇：知识图谱推理与 Tableau 算法详解 下一篇：secret notes4