用 clingo Python API 计算正常逻辑程序的良基模型(Well-Founded Model):well-founded 示例深度解析
人工智能AI Agent多模态语音AI 应用【免费下载链接】ten-frameworkOpen-source framework for conversational voice AI agents项目地址https://gitcode.com/TEN-framework/ten-framework点击查看免费下载导读本文围绕 TEN-framework 仓库third_party/clingo-sys子模块中提供的 well-founded 示例讲解如何利用 clingo 的 Python 绑定、clingox程序解析工具与networkx图算法为一个正常逻辑程序normal logic program计算其良基模型well-founded model。读完本文你将掌握良基模型的三值语义true / false / unknown如何判定、#external声明与负循环、无事实互依赖规则在良基语义下的表现以及基于强连通分量SCC分解与双通道传播事实传播 来源传播的参考实现细节并能直接复现该示例的运行输出。什么是良基模型三值逻辑下的程序语义一个正常逻辑程序由形如head :- body.的规则构成其中规则体可以包含默认否定not。对于这样的程序经典答案集语义要求每个原子要么为真要么为假但对于包含负循环如x :- not x.或互相依赖而无事实支撑的程序经典语义要么无模型要么需要引入未必直观的假设。良基模型well-founded model是 van Gelder、Ross 与 Schlipf 提出的三值模型程序中的每个原子最终被归入以下三种状态之一true事实能够被程序规则正向证明的原子false假不存在任何可证明路径支撑其为真的原子unknown未知既无法证明为真、也无法判定为假的原子典型来源是互相依赖且无事实支撑的规则环或互相否定的规则对。本示例输出的正是前两类中的真原子与未知原子。原 README 明确说明不打印 false 原子原因是在良基语义下凡是未被证明为真的原子都被视为假而这样的原子在开放域中通常是无穷多个逐一列出没有意义。这一点在 well-founded.py 的出口处得到印证函数只构造fctfacts与uknunknowns两个集合并把它们分别打印。原 README 附有一段值得注意的免责声明编写高效计算良基模型的算法其实相当棘手该示例并未经过充分测试可能仍有 bug。因此它更适合作为教学参考与算法原型而不是生产级求解器实现。示例程序逐行解读示例携带的 example.lp 刻意组合了多种语义形态的规则用来覆盖良基模型的不同判定分支#external a. a :- b. b :- a. x :- not x. x :- y. y :- x. u :- not v. v :- not u. r. r :- s. s :- r.规则组语义形态良基模型判定结果#external a.a :- b./b :- a.外部原子声明 无事实支撑的互依赖环a无来源保持未知见下文输出说明x :- not x./x :- y./y :- x.含负循环的规则环x、y无法获得支持来源判定为未知u :- not v./v :- not u.互相否定、无事实支撑u、v均为未知r./r :- s./s :- r.存在事实r的正循环r为事实s因s :- r.可由r证明也归入事实#external是 clingo 中声明外部原子的指令这类原子在接地grounding时不被程序本身决定而是由外部环境如增量求解中的假设赋值。关于外部原子的更多用法可参考同目录下的 external 示例。为什么输出里没有aREADME 的运行输出中 Facts 是r sUnknown 是u v x ya没有出现。从 well-founded.py 的实现看unknowns 的收集要求原子必须出现在prg.output_atoms即被ProgramObserver记录的、出现在规则头中的原子中而a只在#external声明中出现、未作为任何规则的头出现因此不进入输出集合。可以推断这是clingox的ProgramObserver仅记录规则相关符号所致并非a被判定为真或假。运行方式与输出解读安装依赖示例除 clingo 本身外还依赖clingox提供程序解析与ProgramObserver和networkx提供图算法。README 给出的安装命令为python3 -m pip install --user --upgrade --extra-index-url https://test.pypi.org/simple/ clingo-cffi clingox python3 -m pip install --user --upgrade networkx注意clingox需要从测试 PyPI 索引安装--extra-index-url指向test.pypi.org/simple这是该包当前发布渠道的事实实际使用时请以对应索引上的最新版本为准。运行命令与输出在示例目录下执行python well-founded.py example.lpREADME 记录的输出为level version 1.0 Reading from example.lp Facts: r s Unknown: u v x y Solving... UNSATISFIABLE Models : 0 Calls : 1 Time : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.001s这段输出中level version 1.0来自 LevelApp 自定义的program_name与versionFacts: r s与Unknown: u v x y是程序计算出的良基模型分类结果随后Solving... UNSATISFIABLE与Models: 0表明示例在打印完良基模型后仍以经典方式调用ctl.solve()求解而该程序在经典答案集语义下没有稳定模型负循环x :- not x.与互相否定对u/v使得不存在满足所有规则的解释因此求解结果不可满足。良基模型的未知与经典语义的无模型是两种不同视角这一对照正是示例刻意展示的。源码原理SCC 分解 双通道传播well-founded.py 的算法骨架清晰分为三个阶段。阶段一_analyze—— 规则依赖图的强连通分量分解_analyze首先为每条规则建立规则依赖图dep_graph节点是规则编号若规则u的头出现在规则v的体中则添加边u - vwell-founded.py L19-L31。随后用networkx的strongly_connected_components求出强连通分量SCC再构建SCC 之间的依赖图最后按topological_sort得到拓扑序下的规则分组well-founded.py L33-L53。之所以要先做 SCC 分解是因为良基模型可以逐分量独立求解无环的程序可直接由事实正向传播而环内原子必须整体判定是否有外部支撑来源这正是_well_founded要处理的核心。源码注释也点明这里重建 SCC 依赖图只是为了不依赖networkx的组件返回顺序理论上 Tarjan 算法天然给出拓扑序。阶段二_well_founded—— 事实传播与来源传播对每个 SCC 内的规则集合_well_founded维护两套并行的传播机制well-founded.py L56-L166事实传播forward propagation of facts对每条规则统计其体中尚未被证明为真的文字数counters当某规则体全部为真时把它的头文字入队enqueue_lit。这本质上是对程序进行自底向上的最小模型正向闭包计算。来源传播source propagation核心概念是has_source/can_source/is_source。一个文字若既非假、又非真、也未失去来源则可能作为支撑来源当规则体中的文字都获得来源或本身为真时规则头获得来源。若某原子失去了全部来源其规则体中出现了确定为假的文字则把它推入unfounded最终置为假well-founded.py L159-L166。用这个框架理解 example.lpr.是事实经s :- r.把s也推为真a/b与x/y的环没有任何事实或来源注入无法获得has_source因此不被判真u :- not v.与v :- not u.互相否定同样无法建立来源最终三者全部落入 unknown。阶段三well_founded入口与LevelApp应用壳顶层函数well_founded(prg)先做规则形式校验只接受头长度为 1 且非 choice 规则的 normal rules拒绝 weight ruleswell-founded.py L176-L180然后按拓扑序逐 SCC 调用_well_founded最后汇总 facts 与 unknownswell-founded.py L169-L201。LevelApp继承自clingo.application.Application展示了用 clingo Python API 编写命令行求解器的标准姿势well-founded.py L204-L226ctl.register_observer(ProgramObserver(prg))在求解前拦截并记录程序结构ctl.load(f)/ctl.ground([(base, [])])加载并接地程序计算并打印Facts/Unknownctl.solve()继续以经典语义求解得到上述 UNSATISFIABLE 结果sys.exit(clingo_main(LevelApp(), sys.argv[1:]))以自定义应用壳启动。局限性与适用前提仅支持正常规则choice 规则、权重规则都会触发RuntimeError(only normal rules are supported)使用时需自行保证输入程序形态算法效率与健壮性原 README 已声明该实现不是很好测试、可能有 bug适合作为理解良基模型计算过程的参考实现而非大规模程序的求解方案输出语义输出只含 facts 与 unknowns不含 false 原子未出现在output_atoms中的符号如纯#external声明不会被列出。在仓库中的位置本示例位于 third_party/clingo-sys 子模块是 TEN-framework 以第三方依赖形式引入的 clingo Rust 绑定Rust crate及其上游源码包的一部分位于上游examples/clingo/well-founded/目录。同目录下的其他示例如 consequences 展示模型拦截、external 展示外部原子可以与本示例对照阅读共同构成 clingo 编程接口的完整学习素材。小结通过本示例可以一次掌握三件事良基模型三值判定的直观语义、如何用 clingo Python API clingox观察程序结构以及SCC 分解 事实/来源双通道传播这一计算良基模型的经典算法骨架。即使示例本身带有测试不充分的警示它依然是把抽象的逻辑程序语义转化为可运行代码的极佳教学起点。赞分享人工智能AI Agent多模态语音AI 应用【免费下载链接】ten-frameworkOpen-source framework for conversational voice AI agents项目地址https://gitcode.com/TEN-framework/ten-framework点击查看免费下载相关推荐clingo 的 austere 逻辑程序用 reify 元编码计算稳定模型clingo 的 austere 逻辑程序用 reify 元编码计算稳定模型 导读 本文围绕 clingo 仓库中 austere 示例 https://li人工智能AI Agent多模态语音AI 应用clingo 元编程实战用 Reify 与 Meta-Encoding 计算逻辑程序的经典模型Classical Modelsclingo 元编程实战用 Reify 与 Meta Encoding 计算逻辑程序的经典模型Classical Models 导读 在 Answer S人工智能AI Agent多模态语音AI 应用使用 clingo 元编程计算逻辑程序的 Supported Models 实战指南使用 clingo 元编程计算逻辑程序的 Supported Models 实战指南 导读 本文围绕 TEN framework 仓库中随附的 clingo 求人工智能AI Agent多模态语音AI 应用上一篇SDE-Interview-Questions面试策略如何利用题库制定个性化面试准备计划下一篇YOLO_tensorflow模型评估方法mAP计算与性能指标分析终极指南创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考