企业官网建设流程全解析

简介：这份课程设计资料围绕重言式判别程序展开，面向正在学习数据结构与算法、需要完成逻辑表达式相关课设的高校学生。内容以布尔表达式为对象，讲解如何用二叉树组织变量及与、或、非等运算符，并借助后序遍历和栈完成表达式求值，从而判断其是否为恒真式；同时涉及自定义表达式输入、测试用例设计与课程设计文档编写，适合作为课设参考和算法综合练习。压缩包共4个文件，包含2份doc设计文档和2份C语言源码，整体约38KB，文档用于梳理设计思路、算法描述与测试结果，源码便于对照实现细节。目前已有383人学习，读者可从中获得二叉树建树、遍历求值、栈辅助计算、交互设计与文档组织的完整参考。

1. 重言式判别程序课程设计：一行题目背后藏着三个判定引擎

题目发下来只有一句话：编程判断任意给定的命题公式是不是重言式。重言式判别程序课程设计看上去像一次词法分析练习——读字符串、建树、求值，三步走完。真动手才发现，卡住人的从来不是解析，而是判定这一步该怎么收场。五个变元手算真值表还能撑住，十个变元就是 1024 行，二十个变元是 104 万行，靠人眼对数早就崩了。

这个题目的价值在于它逼着你在两条完全不同的路里做选择：一条是老老实实枚举所有赋值，另一条是把「恒真」翻译成「否定式不可满足」，再用归结去反驳。前者好写但会撞上天花板，后者聪明但会撞上子句爆炸。课程设计真正要交的，不是一段能跑通的代码，而是你能说清楚这两条路各自在哪里失效、边界参数怎么定。下面按我实际写过的顺序拆：先做解析，再做真值表引擎，再做归结引擎，最后用随机公式互相对拍。

2. 从字符串到语法树：把 ¬ ∧ ∨ → ↔ 拆成能给程序吃的 token

命题公式在纸面上是二维的，程序里必须先压成一维。这一步的产出是一棵语法树，后面的两个判定引擎都只认这棵树，不认原始字符串——这个约束很关键，它保证了解析只写一次，判定逻辑可以换着写。很多人图省事，在求值函数里直接扫字符串，写着写着就发现真值表引擎和归结引擎各自长出了一套解析代码，改一个优先级要改两处，血泪经验。

2.1 优先级和结合性先钉死，再谈代码

命题逻辑的五个联结词有公认的优先级，麻烦在于「太熟了反而容易写错」。¬ 最高，依次是 ∧、∨、→，↔ 最低。结合性更容易翻车：∧ 和 ∨ 左结合，→ 右结合，也就是说p→q→r必须解析成p→(q→r)，而不是(p→q)→r。这两个式子不等价，前者在 p 假时恒真，后者不是。

允许一个联结词有多种写法不是为了炫技，是因为输入来源太杂：教材用¬，键盘上顺手敲!，从别处复制过来的公式可能是->。词法层把它们归一到同一个 token 类型，语法层就完全不用关心用户到底敲的是哪个符号。这张表要写进代码的注释里，后面每一层递归函数都对着它写。

2.2 递归下降解析器：六个方法吃掉一条公式

递归下降的好处是代码结构和文法一一对应，读代码等于读文法。我一般把文法先写在纸上：

formula := iff EOF iff := imp ( '↔' imp )* imp := or ( '→' imp )? // 右结合，递归而非循环 or := and ( '∨' and )* and := not ( '∧' not )* not := '¬' not | atom atom := VAR | '(' iff ')'

注意imp那一行：它是全篇唯一用递归实现的一层，其余都是 while 循环。这个差别就是右结合和左结合在代码里的全部体现，写反了语法树形状就变，而语法树一错，后面的判定结果全错，还很难查。

import re # 长的写法必须排在短的前面，否则 '<=' 会被 '<=>' 抢先切走一半 TOKEN_SPEC = [ ('IFF', r'<->|<=>|↔'), ('IMP', r'->|=>|→'), ('AND', r'∧|&'), ('OR', r'∨|\|'), ('NOT', r'¬|!|~'), ('LP', r'\('), ('RP', r'\)'), ('VAR', r'[A-Za-z][A-Za-z0-9_]*'), # 允许多字符变量名 p1、rain ('SPACE', r'\s+'), ] def tokenize(s): """把原始字符串切成 (类型, 原文) 的列表，末尾补 EOF 哨兵。""" tokens, pos = [], 0 while pos < len(s): for kind, pat in TOKEN_SPEC: m = re.match(pat, s[pos:]) if m: if kind != 'SPACE': # 空白只消耗，不产生 token tokens.append((kind, m.group(0))) pos += m.end() break else: raise SyntaxError(f'位置 {pos} 出现无法识别的字符 {s[pos]!r}') tokens.append(('EOF', '')) # 哨兵，防止解析越过结尾 return tokens

tokenize里最容易忽略的是for...else：break只在匹配成功时走，else分支只在整轮没匹配上时执行，正好用来报「非法字符」。这个写法比维护一个matched布尔量干净。EOF 哨兵则决定了后面解析器的边界——没有它，peek()会在输入耗尽时抛 IndexError，而不是给出一个可解释的语法错误。

class Parser: def __init__(self, tokens): self.toks, self.i = tokens, 0 def peek(self): return self.toks[self.i][0] def eat(self, kind): if self.peek() != kind: raise SyntaxError(f'期望 {kind}，实际是 {self.peek()}') tok = self.toks[self.i] self.i += 1 return tok def parse(self): node = self.iff() if self.peek() != 'EOF': # 关键校验：不能有剩余字符 raise SyntaxError('公式结束后还有多余字符') return node def iff(self): node = self.imp() while self.peek() == 'IFF': self.eat('IFF') node = ('iff', node, self.imp()) # 左结合，循环累积 return node def imp(self): node = self.or_() if self.peek() == 'IMP': self.eat('IMP') return ('imp', node, self.imp()) # 右结合，递归下降 return node def or_(self): node = self.and_() while self.peek() == 'OR': self.eat('OR') node = ('or', node, self.and_()) return node def and_(self): node = self.not_() while self.peek() == 'AND': self.eat('AND') node = ('and', node, self.not_()) return node def not_(self): if self.peek() == 'NOT': self.eat('NOT') return ('not', self.not_()) # ¬ 可以连写：¬¬p return self.atom() def atom(self): if self.peek() == 'VAR': return ('var', self.eat('VAR')[1]) if self.peek() == 'LP': self.eat('LP') node = self.iff() # 括号里是完整公式，回最高层 self.eat('RP') return node raise SyntaxError(f'位置 {self.i} 期望变量或左括号，实际是 {self.peek()}')

语法树用嵌套元组表示，第一项是节点类型，后面是子节点。这种表示丑但极其省事：节点类型就是字符串，比较、打印、序列化都不用写额外的类；copy.deepcopy都能直接工作。对课程设计这个体量来说，比定义五六个 dataclass 更划算。

atom里括号内的self.iff()是全篇唯一一次「回头调用最高优先级」，也是递归下降能处理任意嵌套的关键。这行写错成self.or_()，就会导致(p→q)在括号里只解析出p，然后eat('RP')直接报错，还以为是括号匹配的问题。

2.3 词法层的输入容忍度：全角符号、空格和大小写

中文输入法下打出来的括号是全角的（），从教材 PDF 复制过来经常带着不可见空格。这两种输入在tokenize里都会掉进「无法识别」的分支。与其让用户自己排查，不如在词法前做一次归一化，代价是几行映射表。

FULLWIDTH = str.maketrans({ '（': '(', '）': ')', ' ': ' ', '！': '!', '＆': '&', '｜': '|', '～': '~', }) def normalize(s): """全角转半角，把常见的中文标点折回 ASCII，再做一次驼峰降级。""" return s.translate(FULLWIDTH)

只做一次translate，不要在这个函数里干别的。变量名大小写不能折叠——P和p在命题逻辑里默认是两个不同的命题变元，把大小写归一了会让P∧¬p从可满足直接变成矛盾式，判定结果天差地别。这个坑非常隐蔽，因为大多数测试用例都只用单一种大小写，只有老师随手敲一条P→p才会暴露。

词法层还要守住一条线：不认识的字符必须报错并给出位置，不能跳过。跳过字符的后果是p @ q被静默读成p和q两个相邻变量，解析器在q那里报「期望运算符」，错误信息指向的位置离真正的问题隔了好几个字符，排查时间直接翻倍。

3. 真值表引擎：2 的 n 次方行枚举，怎么把最坏情况按住

语法树拿到手之后，第一个能落地的判定器就是真值表。思路朴素到没有技术含量：一条公式最多涉及 n 个变元，每个变元取真或假，一共 2^n 种赋值，逐个代进去算，全为真就是重言式，找到一个假就不是。这个方法的好处是永远不会给出错误答案，坏处是它的复杂度增长曲线在 n 超过某个值之后会直接立起来。

代码写起来短，但要写得能跑满 20 个变元，细节全在三处：变量怎么收集、赋值怎么编码、求值怎么短路。

3.1 变量收集与赋值编码：bitmask 映射到 env

第一步是把语法树里出现过的所有变元挖出来。这步必须递归到底，特别注意not节点——¬p里的p也是一个变元，漏掉它会导致真值表少一行，而少的那一行恰好可能是唯一的反例。这类 bug 的症状极其迷惑：公式明明是重言式，程序说不是，换个写法又是对的。

def collect_vars(node, acc=None): """递归收集所有命题变元，返回按字典序排好的列表。""" if acc is None: acc = set() op = node[0] if op == 'var': acc.add(node[1]) elif op == 'not': collect_vars(node[1], acc) # ¬ 下的变元也算 else: collect_vars(node[1], acc) collect_vars(node[2], acc) return sorted(acc)

排序不是可有可无的。真值表的输出顺序、变量和 bit 位的对应关系、两个引擎对拍时的赋值一致性，全都依赖这个顺序固定下来。用 set 直接迭代在 Python 里每次都可能不同，调试时会看到「同一个公式跑两次结果不一样」这种玄学现象。

赋值用整数掩码编码，第 i 位对应第 i 个变量，0 为假、1 为真。这样range(1 << n)就把所有赋值遍历完了，不需要额外的递归或 itertools。

def evaluate(node, env): """在给定赋值 env 下求公式真值。and/or 天然短路。""" op = node[0] if op == 'var': return env[node[1]] if op == 'not': return not evaluate(node[1], env) if op == 'and': return evaluate(node[1], env) and evaluate(node[2], env) if op == 'or': return evaluate(node[1], env) or evaluate(node[2], env) if op == 'imp': return (not evaluate(node[1], env)) or evaluate(node[2], env) if op == 'iff': return evaluate(node[1], env) == evaluate(node[2], env) raise ValueError(f'未知节点类型 {op}')

蕴含和双蕴含的求值式要单独记：A→B等价于¬A∨B，A↔B等价于两者真值相等。这两行如果图快写成evaluate(A) <= evaluate(B)，在布尔值上恰好也对，但只要中间插入任何非布尔的中间结果就会炸，属于能跑但不该跑的写法。

and和or那两行之所以快，是因为 Python 的and/or是惰性求值：左边为假，and右边的evaluate根本不会被调用，整棵子树被跳过。一次局部剪枝看起来微不足道，在 2^20 行的循环里累计起来就是一倍以上的差距。

3.2 短路求值加提前退出：一行反例就够判非重言式

判重言式和打印真值表是两件互相冲突的事。打印要求把 2^n 行全部列出来，一行都不能少；判别只要求找到一个使公式为假的赋值，找到就能收工。课程设计常常两个要求一起提，很多人就写成「先枚举全部再检查」，白白丢掉了提前退出的机会。

def is_tautology_truth_table(node, limit=24): """返回 (是否重言式, 反例赋值)。找到反例立即返回，不遍历全表。""" vs = collect_vars(node) n = len(vs) if n > limit: raise ValueError(f'变元数 {n} 超过真值表上限 {limit}') for mask in range(1 << n): env = {v: bool((mask >> i) & 1) for i, v in enumerate(vs)} if not evaluate(node, env): return False, env # 一行反例，直接出结论 return True, None

mask >> i & 1这一句从低位往高位取，配合vs的排序，保证第 i 个变量对应第 i 个 bit。这个对应关系必须和打印真值表时用的一致，否则人工核对时会发现「程序说 p 真 q 假，表里却是 p 假 q 真」——不是算错，是对齐反了。

提前退出带来的加速不是线性的，是指数级的量级差异被压成常数。构造一个p ∧ q ∧ r ∧ ...那种合取式，第一个赋值全假就使整个公式为假，程序第一轮直接返回。反过来，如果公式确实是重言式，就没有任何捷径，2^n 行必须走满。所以真值表引擎的耗时上限，只在「是重言式」这一侧被真正触发。

要做完整的真值表打印，就再写一个平行函数，循环体里把env和evaluate的结果攒进列表，最后统一格式化输出。两个函数共享collect_vars和evaluate，只是外层循环的收尾条件不同。不要试图用一个early_exit=True参数把两者揉在一起，那个参数会传染到每一行，读起来比写两遍更累。

3.3 真值表法画出的边界：n 到多少就该换引擎

把复杂度摊开算一遍，边界自然就出来了。设公式语法树的节点数为 k，单行求值最坏 O(k)，总复杂度 O(k·2^n)。实际代码里常数因子大概在几十纳秒的量级，但决定性的还是那个 2^n。

n=20 那一行是分水岭：几千万次求值，解释型语言跑起来要几秒到十几秒，还在可接受范围；n=24 直接上到十亿量级，程序会卡到让人以为死循环。所以我把limit默认设成 20 到 24 之间，超了必须抛异常而不是硬跑。抛异常看着不优雅，但比让评分的人对着一个假死的窗口等三分钟要好。

超过这个边界，能做的优化其实不多。可以把语法树编译成逆波兰序列用栈求值，省掉递归的函数调用开销，实测能快两到三倍，但阶数没变。真正的出路只有换算法——这就轮到归结法上场了，它对结构规整的公式根本不需要枚举赋值。

4. 归结反驳引擎：把「恒真」翻成「否定式不可满足」

真值表是正向验证：所有赋值都为真，则公式是重言式。归结法走的是反向：先假设公式为假，也就是取它的否定¬A，然后证明这个否定式不可能被满足。如果¬A不可满足，那么A在所有赋值下都真，A 就是重言式。

这条路的代价是每次归结都要在子句集上做两两配对，但收益也很明显：它不关心变元总数，只关心子句的结构。一个 30 个变元、但子句集只有几条短子句的公式，归结法几毫秒就出结果，真值表要跑到天荒地老。

麻烦的地方在于从语法树走到子句集这一段，中间要经过消蕴含、推否定、展分配三个变换，每一步都可能把公式撑大。

4.1 消蕴含、推否定、展分配：三步走到 CNF

第一步把→和↔全部消掉，只留¬ ∧ ∨。这一步是安全的，公式大小最多翻几倍。

def eliminate(node): """消去 → 和 ↔，只保留 ¬ / ∧ / ∨。""" op = node[0] if op == 'var': return node if op == 'not': return ('not', eliminate(node[1])) if op in ('and', 'or'): return (op, eliminate(node[1]), eliminate(node[2])) if op == 'imp': a, b = eliminate(node[1]), eliminate(node[2]) return ('or', ('not', a), b) # A→B ==> ¬A∨B if op == 'iff': a, b = eliminate(node[1]), eliminate(node[2]) return ('and', # A↔B ==> (¬A∨B)∧(¬B∨A) ('or', ('not', a), b), ('or', ('not', b), a)) raise ValueError(f'未知节点类型 {op}')

双蕴含那条展开式用的是「两个方向都要成立」的写法，比(A∧B)∨(¬A∧¬B)更好，因为它直接产出了两个短子句，后面分配的时候不容易炸。

第二步把否定推到变元上，得到否定范式 NNF。核心是德摩根律：¬(A∧B)变成¬A∨¬B，¬(A∨B)变成¬A∧¬B，遇到¬¬直接剥掉。

def to_nnf(node, neg=False): """neg 表示当前是否处在一个否定的作用域内。""" op = node[0] if op == 'var': return ('not', node) if neg else node if op == 'not': return to_nnf(node[1], not neg) # 双否定相消 if op in ('and', 'or'): if neg: # 德摩根：与或互换 flipped = 'or' if op == 'and' else 'and' return (flipped, to_nnf(node[1], True), to_nnf(node[2], True)) return (op, to_nnf(node[1]), to_nnf(node[2])) raise ValueError('NNF 之前必须先调用 eliminate')

用一个neg布尔参数往下传，比「推完再翻转」的写法少一半节点。这个技巧值得记住，因为任何一次多余的翻转都会在后面的分配阶段被放大。

第三步用分配律把公式压成合取范式，也就是「一堆子句的与」，每个子句是「一堆文字的或」。这是唯一会爆的一步。

def to_cnf(node): """NNF 转 CNF：把 or 分配到 and 上。""" op = node[0] if op in ('var', 'not'): return node if op == 'and': return ('and', to_cnf(node[1]), to_cnf(node[2])) a, b = to_cnf(node[1]), to_cnf(node[2]) # op == 'or' if a[0] == 'and': return ('and', to_cnf(('or', a[1], b)), to_cnf(('or', a[2], b))) if b[0] == 'and': return ('and', to_cnf(('or', a, b[1])), to_cnf(('or', a, b[2]))) return ('or', a, b)

to_cnf里的两次递归调用是重复计算的来源，也是指数膨胀的来源。公式(a₁∧b₁)∨(a₂∧b₂)∨…∨(aₙ∧bₙ)分配之后会得到 2ⁿ 个子句，n=20 时就是一百万条子句，内存直接爆掉。递归里的to_cnf被重复调用了两次，同一个子树算两遍，也让实际耗时比理论值更难看。

真要在这种输入上跑，正确的做法是换 Tseitin 编码：给每个子公式引入一个辅助变元，把它「当且仅当」原公式写成几条子句，整个过程是线性的，代价是变元数增加。Tseitin 不保持逻辑等价但保持可满足性等价，而归结法只需要可满足性，所以完全够用。课程设计如果不强制要求「只用原变元」，这是值得主动加进去的加分项。

4.2 子句集与归结式：frozenset 去重加包含消除

走到 CNF 之后，把它拆成子句集。与节点递归下去，或节点这边把整条链上的文字收成一个集合。文字用带符号的字符串表示：正文字是p，负文字是-p。这样判断互补只要拼一个减号，比维护(name, sign)元组省事。

def literals(node, sign=True, out=None): """把一条 CNF 子句拆成文字集合。""" if out is None: out = set() if node[0] == 'var': out.add(node[1] if sign else '-' + node[1]) elif node[0] == 'not': literals(node[1], not sign, out) elif node[0] == 'or': literals(node[1], sign, out) literals(node[2], sign, out) else: raise ValueError('子句里不应该出现 and') return frozenset(out) # frozenset 才能塞进 set def collect_clauses(node, acc=None): """CNF 树转子句集，重复子句自动合并。""" if acc is None: acc = set() if node[0] == 'and': collect_clauses(node[1], acc) collect_clauses(node[2], acc) else: acc.add(literals(node)) return acc

frozenset这个选择是强迫的：内部子句要用哈希去重，普通set不可哈希。用元组也可以，但元组没顺序保证，还得自己排序，反而更乱。

归结规则只有一条：两个子句里如果存在一对互补文字，把它们各自删掉，剩下的并起来就是归结式。如果两个子句恰好只差这一对互补文字，归结式就是空子句，代表推出了矛盾。

def resolve(c1, c2): """找一对互补文字做归结，找不到返回 None。""" for lit in c1: comp = lit[1:] if lit.startswith('-') else '-' + lit if comp in c2: return (c1 - {lit}) | (c2 - {comp}) return None

resolve只返回第一个找到的归结式，而不是所有可能的。严格说两个子句可能有多对互补文字，应该产生多个归结式。实践里只取一个也够用——因为只要子句集最终饱和，漏掉的那几个归结式总会在别的配对里被补出来。这个取舍能省掉大量重复子句，是让程序能跑完的关键。

4.3 饱和归结什么时候停：空子句、无新子句、规模上限

主循环是一个饱和过程：每轮把当前子句集两两归结，产生的新子句加进去，直到某种终止条件触发。

def is_tautology_resolution(node, max_clauses=20000): """归结反驳：¬A 不可满足 <=> A 是重言式。""" neg = ('not', node) f = to_nnf(eliminate(neg)) # 先取否定，再化 NNF cnf = to_cnf(f) clauses = collect_clauses(cnf) if frozenset() in clauses: # 否定式本身含空子句，直接恒真 return True while True: current = list(clauses) new = set() for i in range(len(current)): for j in range(i + 1, len(current)): r = resolve(current[i], current[j]) if r is None: continue if len(r) == 0: # 推出空子句，不可满足 return True if any(c <= r for c in clauses | new): continue # 包含消除：已被更短子句吸收 new.add(r) if not new: # 饱和且无空子句，可满足 return False clauses |= new if len(clauses) > max_clauses: raise RuntimeError(f'子句数超过 {max_clauses}，判定中止')

三个终止条件各自对应一种结局。空子句出现，意味着从¬A推出了矛盾，¬A不可满足，A是重言式。新子句集为空，意味着所有能归结的组合都试过了，没有矛盾，¬A可满足，A不是重言式。子句数超过上限，意味着程序没法在合理时间内给出答案，只能中止——这个分支必须存在，否则一次作业演示就能把内存吃满。

any(c <= r for c in clauses | new)这一行是包含消除，<=在 frozenset 上是子集判断。它的作用是把「已经被更短子句完全覆盖」的新子句丢掉：如果已经有{p}，再产生{p, q}就没有意义，因为{p}更强。不做这一步，子句库会以肉眼可见的速度膨胀，而且膨胀出来的全是废子句。

max_clauses的默认值我一般设在两万左右。这个数字不是算出来的，是试出来的：低于一万，稍微复杂点的公式就中止；高于五万，主循环的两两配对已经是 O(m²)，一秒钟只能推进一步，体验极差。

5. 避坑与排查：重言式判别程序最常翻车的五个地方

代码能跑通和代码能交作业之间，隔着一堆只在特定输入下才现形的问题。下面五条是我自己踩过、也见过别人反复踩的，按「现象 → 原因 → 解决」记下来，方便对着排查。

第一条：优先级写反，p→q∧r被解析成(p→q)∧r。

现象是公式明明是重言式，程序却判成非重言式，而且给出来的反例赋值看着毫无道理——p 真 q 假的时候公式为假，但按正确优先级 p 真 q 假 r 任意时公式应该为真。原因几乎都是imp()里调用了or_()之后，又在同一层把AND吃掉了，或者把→和∧放进了同一层循环。解决办法是把文法写在注释里，然后加一组断言测试：p→q∧r的树必须是('imp', p, ('and', q, r))，p→q→r的树必须是('imp', p, ('imp', q, r))。这两条断言能挡住九成的优先级 bug。

第二条：深层嵌套导致 RecursionError。

现象是输入一条几十个括号嵌套的公式，程序直接抛RecursionError: maximum recursion depth exceeded，连个像样的错误信息都没有。原因是递归下降每一层括号都要往下压一个iff()调用栈，Python 默认递归上限是 1000，嵌套超过 300 层就危险了。解决分两步：解析前先扫一遍括号深度，超过 200 直接报「公式嵌套过深」；同时在入口处sys.setrecursionlimit(10000)兜底。但要注意，调高上限只是延后崩溃，真正的防线是深度检查——否则会从 RecursionError 变成段错误，更难查。

第三条：归结主循环不收敛，程序卡死。

现象是某些公式输入后 CPU 跑满、内存缓慢上涨、几分钟不返回。原因通常是两处：一是新子句没去重，同一对子句每轮都重新归结一遍，产生同样的归结式；二是没有包含消除，{p}和{p,q}这类冗余子句越积越多，下一轮两两配对的组合数按平方增长。解决就是前面代码里的两行——用set存子句、用c <= r做吸收，再加一个max_clauses上限强制中止。上限那条不能省，它是唯一能保证程序一定返回的东西。

第四条：CNF 分配阶段内存爆掉。

现象是公式看着不长，但在to_cnf里跑着跑着内存就上去了，最后 MemoryError。原因是分配律展开是指数的，(a₁∧b₁)∨(a₂∧b₂)∨…这种形状在 n 到 20 左右就产生上百万个子句。解决有两条路：一是加规模预判，在to_cnf之前先统计or节点下面挂了多少个and节点，超过阈值就抛出可读的异常；二是换 Tseitin 编码，用辅助变元把转换压到线性。课程设计里第一种就够交差，第二种是加分项。

第五条：空输入、多余字符、括号不匹配导致的各种崩。

现象五花八门：输入空串报IndexError，输入p q报「期望运算符」但位置指错，输入(p∧q直接抛到解释器。根因都一样——解析器没有在边界上做检查。parse()结束必须确认peek() == 'EOF'，否则p q会被当成解析成功然后剩下一个q没人管；atom()里遇到RP或者EOF必须给出明确错误，而不是继续递归；输入为空要在tokenize之后立刻判断，因为这时候 token 列表里只有 EOF 哨兵，iff()一路往下会在atom()里撞墙。

提示：这五条里，第一条和第五条会直接导致结果错误，第三条和第四条会导致程序挂死，第二条介于两者之间。排查顺序建议先跑一组手算过的小公式（三到五个变元）验证正确性，再上大公式压性能，不要一上来就测复杂用例。

6. 随机公式对拍：怎么证明两个判定引擎都没写错

两个引擎写完了，最怕的是它们「看起来都对」。手写的测试用例总是覆盖不到自己想不出的边界，这时候唯一可靠的办法是随机生成公式，让两个引擎各自判定，比对结果。

生成器不用太聪明，递归往下造就行，关键是控制深度和变元池，保证生成的公式不会在 CNF 转换阶段直接爆掉。

import random def random_formula(depth, pool): """随机造一棵语法树，depth 控制嵌套层数。""" if depth <= 0 or random.random() < 0.3: return ('var', random.choice(pool)) op = random.choice(['not', 'and', 'or', 'imp', 'iff']) if op == 'not': return ('not', random_formula(depth - 1, pool)) return (op, random_formula(depth - 1, pool), random_formula(depth - 1, pool)) def <p> <a href="https://download.csdn.net/download/songkaisong/1326707" style="color:#ec7500;font-size:14px;"> 本文还有配套的精品资源，点击获取 </a> <img alt="menu-r.4af5f7ec.gif" src="https://csdnimg.cn/release/wenkucmsfe/public/img/menu-r.4af5f7ec.gif" style="width:16px;margin-left:4px;vertical-align:text-bottom;cursor:text;"> </p>