clingo 的 austere 逻辑程序：用 reify 元编码计算稳定模型

• 人工智能
• AI Agent
• 多模态
• 语音
• AI 应用

导读

本文围绕 clingo 仓库中 austere 示例 展开，介绍一类特殊的逻辑程序——austere logic programs（"austere" 意为"朴素/极简"，此处特指程序中默认否定not只出现在约束规则中的程序）。文章将带你理解这类程序的意义，掌握clingo --output=reify物化（reify）输出与meta.lp/encoding.lp元编码配合的完整求解调用链，并通过逐行拆解元编码，解释其如何用"约束"替代"规则体中的默认否定"来定义稳定模型。读完本文，你将能够独立运行并扩展这套元求解方案，理解 Answer Set Programming（ASP）中"用元程序解释程序"的经典思路。

austere 逻辑程序：默认否定只出现在约束中

在经典 Answer Set Programming 中，稳定模型（stable model）的定义依赖"程序约简"（program reduct）：对程序P与解释X，将P中规则体里所有被X满足的默认否定文字删除，得到约简P^X，再要求X恰好是P^X的最小模型。这一过程把"默认否定"内嵌到了每一条规则里。

Austere 逻辑程序则是一种更受限、也更"干净"的形式：程序中的所有默认否定not都只出现在约束（constraint）中，即出现在形如

:- not a, b.

的规则里，而普通规则（正规则、析取规则、选择规则、加权和规则）中不再出现not。这样，稳定模型的语义可以绕开复杂的"最小模型 + 约简"操作，退化为一个更朴素的条件：候选模型必须满足程序中的所有约束，而满足约束的结果天然对应原程序的稳定模型。

仓库中的示例程序 example.lp 是一个经典的双否定循环：

a :- not b. b :- not a.

这个程序有两个稳定模型：{a}与{b}。但它并不是 austere 形式——两条规则体中都带有not。其 austere 等价的思路是：把"默认否定"语义迁移到约束层，由元编码统一处理。

整体求解调用链：reify + 元编码

示例 README 给出的一行命令即可完成全部稳定模型求解：

$ clingo --output=reify example.lp | clingo -Wno-atom-undefined - encoding.lp 0

这条管道式命令拆解如下：

clingo --output=reify是 clingo 自带的物化后端。它不会直接求解程序，而是把"程序结构"作为数据输出。整个 reify 示例目录（examples/reify）都建立在同一套物化事实格式之上，目录内common/提供了通用元编码 meta.lp，各子目录（simple、classical、ht、austere、optimization、supported、many、gac）则针对不同语义目标提供专门的encoding.lp。

运行该命令，输出即为原程序的两个稳定模型（以show语句选出的原子呈现）：

Answer: 1 a Answer: 2 b

这与直接运行clingo example.lp 0的结果一致，验证了元编码的正确性。

元编码逐行拆解：约束如何取代默认否定

austere 元编码 encoding.lp 的核心设计是：不再在规则体中解释not，而是把每个可能原子拆成hold(A)（为真）与nhold(A)（为假）两个"标志原子"，再强制二者互斥且完备，最后用约束收紧候选集。

规则体求值（只认"正"字面量）

conjunction(B) :- literal_tuple(B), hold(L) : literal_tuple(B, L), L > 0; nhold(L) : literal_tuple(B,-L), L > 0. body(normal(B)) :- rule(_,normal(B)), conjunction(B). body(sum(B,G)) :- rule(_,sum(B,G)), #sum { W,L : hold(L), weighted_literal_tuple(B, L,W), L > 0 ; W,L : nhold(L), weighted_literal_tuple(B,-L,W), L > 0 } >= G.

物化阶段把原规则a :- not b.表达为rule(normal(B), ...)+literal_tuple(B, 1)（正字面量a）+literal_tuple(B, -2)（负字面量not b）。注意此处默认否定已经在物化数据里被"符号化"为负字面量-L，元编码中对应的nhold(L)表示该原子"不成立"。因此conjunction(B)只依赖正字面量对应的hold(L)与负字面量对应的nhold(L)，元程序本身的规则体不再出现not——这就是 austere 语义在元层面的落实。

对于加权和规则rule(sum(B,G), ...)，元编码用#sum聚合所有成立（hold）与不成立（nhold）字面量的权重W，要求总权重不低于阈值G，从而把#sum规则体也翻译为无not的形式。

规则头部的推导

hold(A) : atom_tuple(H,A) :- rule(disjunction(H),B), body(B). { hold(A) : atom_tuple(H,A) } :- rule( choice(H),B), body(B).

• 对析取规则rule(disjunction(H), B)：一旦规则体成立，头部原子元组中至少一个hold(A)必须成立（条件字面量集合的强推导）；
• 对选择规则rule(choice(H), B)：规则体成立时，头部原子集合可以任意选择成立子集（用花括号选择规则表达）。

这两行把原程序中所有"正头规则"的语义搬运过来，且不引入默认否定。

收敛输出

#show. #show T : output(T,B), conjunction(B).

第一行#show.清空默认显示，第二行只输出满足规则体的规则头部原子，避免物化产生的内部谓词（rule/3、hold/1等）污染结果视图。

关键：原子的完备性约束

% atoms that occur negated atom(L) :- literal_tuple(B,-L), L > 0. atom(L) :- weighted_literal_tuple(B,-L), L > 0. % open fresh atoms, and constrain their truth value { nhold(L) } :- atom(L). :- hold(L), nhold(L), atom(L). :- not hold(L), not nhold(L), atom(L).

这是 austere 元编码区别于通用元编码 meta.lp 的关键所在。比较两份编码可以看出：

• 通用版 meta.lp 直接在规则体中使用not hold(L)，例如conjunction(B) :- ... not hold(L) : literal_tuple(B,-L), L > 0.——它把默认否定留在了元程序的规则体内；
• austere 版则先收集所有以负字面量出现的原子atom(L)，为它们"开辟"一个未定标志{ nhold(L) }，再用两条约束强制完备性：

:- hold(L), nhold(L), atom(L). % hold 与 nhold 不可同时成立 :- not hold(L), not nhold(L), atom(L). % 二者必须至少成立其一

注意第二条约束:- not hold(L), not nhold(L), atom(L).自身带有默认否定，但它是约束（头部为空），完全符合 austere 定义中"默认否定只出现在约束中"的要求。这样一来，任何候选模型对每个原子都必须给出"成立/不成立"的唯一判定，等价于经典稳定模型对原子真值的排他性要求；而由于负字面量对应的nhold(L)已被约束钉死，规则体求值时不再需要not，便得到了与原程序稳定模型一一对应的模型集合。

为什么能成立：约束层语义

从语义角度看，:- not a.这类约束在稳定模型语义中等价于强制a成立（否则约简后约束体为空、约束永不满足）。austere 程序的稳定模型因此可以描述为：在"不假设任何负文字成立"的前提下，所有规则产生的模型候选，再经约束筛选后留下的解释。元编码用nhold与两条完备性约束精确复刻了这一过程，这也是 [1] 中 "Answer Set Programming Made Easy" 的核心动机——把稳定模型语义化简为"满足约束的模型"。

实战验证与扩展

验证命令

在仓库的 austere 示例目录内，可以分别查看物化输出与最终结果：

# 1. 查看物化后的"程序事实" clingo --output=reify example.lp # 2. 完整求解：所有稳定模型 clingo --output=reify example.lp | clingo -Wno-atom-undefined - encoding.lp 0

用--text观察 grounding 的影响

与 classical 示例 中提示的一致，grounding 阶段可能引入简化、消除部分原子。可先观察原程序的地面化结果：

clingo --text example.lp

若担心 grounding 简化影响物化事实的完整性，可在原程序中添加外部声明（如#external a.）保留原子，这与 classical 示例example1.lp的做法一致。

横向对照其他 reify 示例

austere 编码与同目录其他元编码共享物化事实格式，可对照阅读：

• simple/README.md：最简元编码，直接复现物化程序的回答集，clingo --output=reify example.lp | clingo -Wno-atom-undefined - ../common/meta.lp 0；
• common/meta.lp：通用元编码，规则体内直接使用not，与 austere 版形成"规则体否定 vs 约束否定"的直观对比；
• ht/README.md：用-c option=1/2/3在同一元编码上切换 Here-and-There 模型、最小化 Here 世界与 Equilibrium 模型；
• optimization/README.md：展示--rewrite-minimize --output=reify --reify-sccs与optimize(0,1,card)/optimize(0,1,incl)配合实现基数最小化与子集最小化，并建议用clingo --pre ... | reify --sccs预处理提升性能。

这些示例共同验证了一个结论：物化（reify）把 clingo 变成了"可以解释任意程序的元解释器"，而 austere 编码则是其中"把否定语义收敛到约束层"的一种优雅实现。

小结

• austere 逻辑程序：默认否定只出现在约束中的程序，其稳定模型可被简化理解为"满足约束的模型"；
• 标准求解调用：clingo --output=reify example.lp | clingo -Wno-atom-undefined - encoding.lp 0，两阶段分别负责物化与元求解；
• 元编码要点：正字面量用hold、负字面量用nhold，规则体求值只依赖正条件；析取/选择/加权和规则分别翻译；最后用两条约束强制hold/nhold互斥且完备，完成对"默认否定"语义的约束化还原；
• 对照价值：与 common/meta.lp 对比，可清晰看到"规则体否定"与"约束否定"两种元编码风格的差异，理解 austere 编码在语义上更贴近 [1] 中"Answer Set Programming Made Easy"的化简目标。

参考资料

[1] Jorge Fandinno, Seemran Mishra, Javier Romero, Torsten Schaub:Answer Set Programming Made Easy（投稿中）——该工作即 austere 逻辑程序元编码的思想来源，示例 README 中明确标注。

相关文件索引（均可从仓库根目录访问）：

• austere 示例 README
• austere 元编码
• austere 示例程序
• 通用元编码
• reify 示例目录

• 人工智能
• AI Agent
• 多模态
• 语音
• AI 应用