重言式判别程序课程设计：公式解析、真值表与CNF推演

简介：这份课程设计资料包围绕重言式判别程序展开，面向学习数据结构与算法、需要完成逻辑表达式课程设计的学生及自学者，重点解决用二叉树表示布尔表达式并判别其是否为恒真式的问题。压缩包共4个文件，包含2个C语言源码和2个Word文档，整体约38KB，源码可用于运行与调试，文档则承载设计说明与课程设计报告。已有383人学习，说明该题目在数据结构实践中具有一定参考需求。资料覆盖二叉树构建、前中后序遍历尤其是后序遍历求值、栈辅助存储中间结果，以及自定义布尔表达式输入与判别等关键环节；文档还涉及项目概述、设计思路、主要算法描述、代码实现细节、测试用例及优化方向，便于读者对照理解程序结构、梳理实现路径并完成自己的课程设计。

1. 一个→引发的误判

某同学把(p→q)∧p→q敲进自己写的重言式判别程序，返回结果是一个「否」。他手算三遍都是真，开始怀疑教材印错了。定位到词法层才发现：程序不认→，公式被截成一个只含q的残片，而q当然不是永真。

重言式判别程序课程设计，核心从来不是「判别」那一步——真值表跑一遍all()就完事。难的是把一串人写的符号完整无歧义地变成机器能算的结构，并且在变量数涨上去之后还跑得动。下面按改代码时看到的顺序走：符号表与语法树、真值表枚举、一条不靠枚举的等价推演路线、五个高频翻车现场，最后是对拍验证。适合正在做这道课设、想把它从「能跑」推到「敢交」的人。

2. 命题公式怎么进程序：符号表、词法与语法树

这一章解决「输入」问题。命题公式不是普通算术表达式，它有五种联结词、四档优先级、两种结合性，还有一堆等价写法（→和->、↔和<->和<=>）。我在看别人代码时，八成以上的错误都出在这一层，而不是后面的算法层。先把这一层做扎实，后面的枚举和推演才有意义。

2.1 五类联结词的优先级与结合性一次定死

优先级不统一，后面全是连锁反应。我一般按下面这张表固定下来，写进常量，别在代码里散落硬编码。

两处容易定错。其一是蕴含：p->q->r在人写数理逻辑时默认右结合，即p->(q->r)；如果按左结合会得到(p->q)->r，这两个式子真值表完全不同，一个反例是p=q=r=假。其二是等价：<->左结合还是右结合其实不影响结果（等价满足结合律），但解析器的写法会影响你调试时看到的树形，建议统一按左结合处理，减少一层递归。

!的优先级高于所有二元联结词，这条必须硬性保证，否则!p & q会被读成!(p & q)——这是第 5 章要单独讲的一个坑。

提示：把这张表直接做成模块级常量PREC，解析器和打印器共用一份，改一处全改，别在两个文件里各写一遍。

2.2 词法切分：<->和->谁先匹配

词法分析的唯一难点是最长匹配。输入里出现<->时，如果先匹配到->，前面那个<就变成非法字符；同理<=>和=>也会打架。解决办法是把所有别名按长度倒序排，逐个尝试前缀匹配。

# 别名统一映射到内部记号，键决定能识别哪些写法 ALIAS = { '!': '!', '~': '!', '¬': '!', 'not': '!', '&': '&', '&&': '&', '∧': '&', '*': '&', 'and': '&', '|': '|', '||': '|', '∨': '|', '+': '|', 'or': '|', '->': '->', '→': '->', '=>': '->', '<->': '<->', '↔': '<->', '<=>': '<->', '(': '(', ')': ')', } # 按长度倒序，保证 '<->' 在 '->' 之前被尝试 KEYS = sorted(ALIAS, key=len, reverse=True) def tokenize(src: str): """把源串切成 (类型, 原文) 序列，类型是 VAR 或内部记号""" toks, i = [], 0 while i < len(src): ch = src[i] if ch.isspace(): # 空白直接跳过，允许任意排版 i += 1 continue if ch.isalpha(): # 变量或单词型联结词 j = i while j < len(src) and (src[j].isalnum() or src[j] == '_'): j += 1 word = src[i:j] if word in ALIAS: # and / or / not 走别名表 toks.append((ALIAS[word], word)) else: toks.append(('VAR', word)) i = j continue for k in KEYS: # 最长匹配，命中即停 if src.startswith(k, i): toks.append((ALIAS[k], k)) i += len(k) break else: raise SyntaxError(f'位置 {i} 出现无法识别的字符 {ch!r}') return toks

这段逻辑有三处值得说明。第一，字母分支放在符号匹配之前，保证not被当成联结词而不是变量n、o、t三个字符；同时也保证not_p这种变量名不被误切。第二，KEYS排序只能做一次，别放进循环里每次排序，公式长的时候这是实打实的开销。第三，报错信息里带上位置索引i，这是后面排查语法错误时唯一的锚点，省掉它等于把黑匣子交给用户。

一个容易忽略的细节：变量名如果恰好叫and，就会被识别成联结词。这在课设里基本不会出现，但如果你允许中文变量名或者单字母以外的标识符，最好在文档里写一句「and/or/not为保留字」。

2.3 递归下降建树：按优先级分层的六个函数

语法树节点用元组表示，形如('var', 'p')、('!', 子节点)、('&', 左, 右)。这种表示轻量、可哈希，后面做缓存和去重都方便。

递归下降的关键是「一层优先级一个函数」，低优先级函数调用高优先级函数。这样调用链本身就编码了优先级，不需要额外的比较逻辑。

class Parser: def __init__(self, toks): self.toks, self.i = toks, 0 def peek(self): return self.toks[self.i] if self.i < len(self.toks) else None def eat(self, kind=None): t = self.peek() if t is None: raise SyntaxError('公式意外结束') if kind and t[0] != kind: raise SyntaxError(f'期望 {kind}，实际 {t[0]}') self.i += 1 return t def parse(self): node = self.p_iff() # 从最低优先级开始 if self.peek() is not None: raise SyntaxError(f'多余的记号 {self.peek()}') return node def p_iff(self): # 优先级 1，左结合 node = self.p_imp() while self.peek() and self.peek()[0] == '<->': self.eat() node = ('<->', node, self.p_imp()) return node def p_imp(self): # 优先级 2，右结合 node = self.p_or() if self.peek() and self.peek()[0] == '->': self.eat() return ('->', node, self.p_imp()) # 右侧递归，实现右结合 return node def p_or(self): # 优先级 3，左结合 node = self.p_and() while self.peek() and self.peek()[0] == '|': self.eat() node = ('|', node, self.p_and()) return node def p_and(self): # 优先级 4，左结合 node = self.p_not() while self.peek() and self.peek()[0] == '&': self.eat() node = ('&', node, self.p_not()) return node def p_not(self): # 优先级 5，右结合 if self.peek() and self.peek()[0] == '!': self.eat() return ('!', self.p_not()) return self.p_atom() def p_atom(self): # 原子：变量或括号 t = self.peek() if t[0] == 'VAR': self.eat() return ('var', t[1]) if t[0] == '(': self.eat() node = self.p_iff() # 括号内重新从最低优先级开始 self.eat(')') # 没闭合就在这里抛错 return node raise SyntaxError(f'原子位置出现 {t}')

p_imp和p_iff的写法差别就是结合性的全部秘密：p_imp用return ('->', node, self.p_imp())，把右侧整体再交给同层函数，得到右结合；p_iff用while循环，把结果不断折叠到左边，得到左结合。p_not同理，!!p要能正确解析成两次否定。

括号的处理有个小陷阱：eat(')')如果失败，报的是「期望)，实际是 XXX」，这比在parse()结尾报「多余的记号」更容易定位。所以括号闭合检查要放在p_atom里，别偷懒放到最外层。

2.4 调度场算法：什么时候它比递归下降更省事

如果你只想求值、不需要保留树结构，中缀转后缀（调度场算法）代码量更小，而且求值时用一个栈循环就够，不需要递归。思路是维护一个运算符栈，遇到操作数直接输出，遇到运算符就把栈顶优先级不低于它的全部弹出，遇到左括号入栈，遇到右括号弹到左括号为止。

但在重言式判别这道课设里，我一般不推荐这条路。原因有三：一是你后面要做 NNF 变换、CNF 展开，这些都需要树结构，转成后缀还得再转回来；二是后置单目运算符（!）在调度场里要特殊判断「是前缀还是中缀」，容易写错；三是调试时打印一棵缩进树远比打印一串后缀直观。只有一种情况值得用它——你确定只需要真值表、不打算做等价推演，那么后缀式数组求值比递归遍历快两倍左右，这在变量数逼近 20 时能省下几十秒。

3. 真值表枚举：2^n 次赋值怎么写得不慢

有了树，最直接的判别方式就是把所有变量赋值组合跑一遍。听起来是笨办法，但它有一个别的办法都没有的优点：给出反例。当程序说「不是重言式」时，真值表能顺手告诉你哪一组赋值让它为假，这在课设答辩现场非常好用。这一章讲怎么把这个笨办法写得不笨。

3.1 变量收集与字典序编号：为什么要单独遍历一遍

很多人图省事，在求值时遇到新变量就动态加进字典，结果变量顺序取决于公式的书写顺序，p&q和q&p拿到的最小项编号完全不同。主析取范式一输出就露馅。

正确做法是先单独遍历一次语法树，把所有变量收进集合，排序后再固定编号：

def collect_vars(node, out=None): """深度优先收集变量名，结果为排序后的列表，保证编号稳定""" if out is None: out = set() if node[0] == 'var': out.add(node[1]) else: for child in node[1:]: collect_vars(child, out) return sorted(out)

sorted()这一步是刻意的。字典序编号意味着同一个公式无论重排多少次书写，变量顺序都一样，主析取范式的最小项列表也就稳定。答辩时老师随手把p&q改成q&p，你的输出不变，这一下就体现了工程素养。

如果公式里一个变量都没有（比如1、p|!p化简后），collect_vars返回空列表，后面枚举range(1 << 0) = range(1)，只跑一次 mask=0，逻辑自然成立，不需要特判。

3.2 位掩码枚举：一个 for 循环替掉递归回溯

枚举 2^n 种赋值，最直觉的写法是递归回溯：对第 i 个变量分别试真和假。但递归深度等于变量数，每个叶子要复制一份完整字典，n=15 时就是 32768 次字典拷贝，白白浪费。

位掩码写法把「第几个变量取真取假」编码进一个整数的二进制位，循环一遍整数就枚举完了：

def eval_node(node, env): """在给定赋值下求值，env 是 {变量名: bool}""" op = node[0] if op == 'var': return env[node[1]] if op == '!': return not eval_node(node[1], env) a = eval_node(node[1], env) b = eval_node(node[2], env) if op == '&': return a and b if op == '|': return a or b if op == '->': return (not a) or b # 蕴含的定义，别写成 a and not b if op == '<->': return a == b # 等价就是布尔相等 raise ValueError(f'未知节点 {op}') def truth_table(node, stop_on_false=False): """返回 (变量列表, [(mask, 取值)])；stop_on_false 用于快速判重言式""" names = collect_vars(node) n = len(names) rows = [] for mask in range(1 << n): # 高位对应排在前面的变量，保证 mask 递增时字典序递增 env = {name: bool((mask >> (n - 1 - i)) & 1) for i, name in enumerate(names)} val = eval_node(node, env) rows.append((mask, val)) if stop_on_false and not val: return names, rows # 找到反例立刻收工 return names, rows

位序那一行(mask >> (n - 1 - i)) & 1是全篇最容易写反的地方。如果写成(mask >> i) & 1，变量顺序就整体反转，最小项编号全部对不上，而且程序不会报错，只会在输出里给你一串看起来合理但错误的结果——这是最阴的一类 bug。判断标准很简单：n=2，变量[p, q]，mask=0 时应为p=假, q=假，mask=3 时应为p=真, q=真。写完后先拿这个例子手验一遍再往下走。

->和<->的求值也值得盯一眼。蕴含只有在前件真、后件假时为假，等价就是两个布尔值相等。这两行如果手滑写成a and not b或者a != b，反例不会报错，但结果是全错的。

3.3 找反例就停：判定重言式的最短路径

判重言式不需要完整的真值表，只需要一个反例。所以stop_on_false=True是最有效的单点优化：绝大多数非重言式公式在第一两个 mask 就能命中，平均耗时从 O(2^n) 掉到 O(1)。

真正跑满 2^n 的只有重言式本身。这时候你要想别的办法：

常量折叠。建树之后先做一遍化简：p & 真 → p、p | 真 → 真、p -> 假 → !p。如果化简结果直接就是常量，立即返回，不用枚举。这一步能干掉大量p | !p形式的平凡重言式。

子式缓存。如果同一个子式在树上出现多次（比如(a&b) | (a&b)），求值时按节点 id 缓存结果，能把重复计算压掉一半。

位并行。当 n ≤ 16 左右，可以给每个变量构造一个 2^n 位的整数掩码，所有赋值同时算。这种做法常数因子极小，但代码复杂度陡增，课设里除非老师点名要求性能，否则没必要上。

变量数上限提示。n 超过 24 时 2^24 ≈ 1600 万次树遍历，Python 里大概要跑几分钟。这时候应该在入口处明确提示「变量数超过上限，建议改用等价推演路线」，而不是让用户盯着黑屏等。这是我的血泪经验：一定要有上限保护，否则答辩现场演示一个 30 变量的公式，程序直接卡死，非常尴尬。

3.4 主析取范式与主合取范式：顺手就出来了

主析取范式就是「所有让公式为真的最小项之析取」，主合取范式就是「所有让公式为假的极大项之合取」。有了真值表，这两个都是几行代码的事：

def canonical_forms(node): names, rows = truth_table(node) n = len(names) minterms = [m for m, v in rows if v] # 为真的行 → 最小项 maxterms = [m for m, v in rows if not v] # 为假的行 → 极大项 def lit(name, positive): return name if positive else f'!{name}' # 最小项：变量按位取，1 用原变量，0 用否定 dnf = ' | '.join( '(' + ' & '.join(lit(names[i], (m >> (n - 1 - i)) & 1) for i in range(n)) + ')' for m in minterms ) or '0' # 空析取记作假 # 极大项：变量按位取，0 用原变量，1 用否定 cnf = ' & '.join( '(' + ' | '.join(lit(names[i], not ((m >> (n - 1 - i)) & 1)) for i in range(n)) + ')' for m in maxterms ) or '1' # 空合取记作真 return sorted(minterms), sorted(maxterms), dnf, cnf

最小项和极大项的取反规则必须记牢：最小项里「为 1 取原变量，为 0 取否定」，极大项恰好相反，「为 0 取原变量，为 1 取否定」。搞反了写出来的范式虽然形式正确，但和标准答案对不上。用空串兜底成'0'和'1'也是必要的：公式恒假时最小项列表为空，join出来是空串，打印出来一片空白，不如显式写成0。

minterms的编号规则也要和教材一致：把变量按字典序排好，真记 1、假记 0，组成二进制数再转十进制。如果你的mask位序和这条规则一致，minterms直接就是编号，不需要任何转换。

4. 等价推演：不枚举也能判的那条路

真值表是万能的，但它的复杂度是指数的。变量数上到 25 以上，枚举就完全不可行了。这时候需要另一条路线：把公式推到某个标准形，用结构判据直接得出结论。这条路线不保证多项式时间（CNF 展开本身可能指数爆炸），但在很多实际公式上远快于枚举。

4.1 先消蕴含再取 NNF：否定下沉的两条规则

第一步是把->和<->消掉，只留!、&、|。这一步是恒等变形，不改变真值：

def eliminate_impl(node): """消去蕴含和等价，只保留 ! & | 和变量""" op = node[0] if op == 'var': return node if op == '!': return ('!', eliminate_impl(node[1])) a = eliminate_impl(node[1]) b = eliminate_impl(node[2]) if op == '->': return ('|', ('!', a), b) # a→b ≡ ¬a∨b if op == '<->': # a↔b ≡ (a→b) ∧ (b→a) return ('&', ('|', ('!', a), b), ('|', ('!', b), a)) return (op, a, b)

第二步是把否定只压到变量上，得到否定范式 NNF。核心是德摩根律：!(a & b) ≡ !a | !b，!(a | b) ≡ !a & !b，而!!a ≡ a。实现上用「负号标记」往下传，避免每层都新建!节点：

def to_nnf(node, neg=False): """neg 表示当前是否处于偶数个否定之下""" op = node[0] if op == 'var': return ('!', node) if neg else node if op == '!': return to_nnf(node[1], not neg) # 双重否定直接消掉 a = to_nnf(node[1], neg) b = to_nnf(node[2], neg) if neg: # 德摩根：翻转运算符 op = '|' if op == '&' else '&' return (op, a, b)

to_nnf写成「带负号标记」的形式，比「每层遇到否定就递归取反」要干净得多，因为它在整个过程中不会产生任何多余的!节点，最后 NNF 树的大小和原树同阶。如果这一步写成朴素的「遇到!就对子树逐个取反再翻转运算符」，很容易在多层嵌套时把节点数翻倍，后面 CNF 展开会被放大成灾难。

4.2 分配律展开成 CNF：子句列表比树好操作

NNF 之后，用分配律a | (b & c) ≡ (a | b) & (a | c)把公式推成合取范式。我在这一步不用树，直接改用「子句列表」：CNF 是若干子句的合取，每个子句是若干文字的析取，用[[(变量, 正负), ...], ...]表示。这种表示让「合并」「判空」「判互补」都变成集合操作。

def cnf_clauses(node): """输入必须是 NNF，输出子句列表，文字形式为 (变量名, 是否为正)""" if node[0] == 'var': return [[(node[1], True)]] if node[0] == '!': return [[(node[1][1], False)]] # ! 只作用于变量 if node[0] == '&': # 合取：两边子句直接拼接，不产生交叉项 return cnf_clauses(node[1]) + cnf_clauses(node[2]) if node[0] == '|': left, right = cnf_clauses(node[1]), cnf_clauses(node[2]) # 析取：两两合并，每对子句做一次「分配」 return [a + b for a in left for b in right] raise ValueError(f'NNF 中不应出现 {node[0]}')

注意|分支的复杂度：左边 k 个子句、右边 m 个子句，结果是 k×m 个。这就是 CNF 的指数爆炸点，(a1&b1) | (a2&b2) | ...这种形式会瞬间炸开。控制办法只有一个——限制变量数和子句数上限，超过就回退到真值表（如果 n 允许）或者直接报「结构过于复杂」。

还有一个容易漏掉的优化：合并两个子句时，如果产物里同时含p和!p，这个子句恒真，整个子句可以直接丢弃（因为它是析取，恒真不提供约束）。这一步能把很多爆炸在半路掐死：

def simplify_clause(clause): """子句内去重；若同时含互补文字对，返回 None 表示恒真可丢弃""" lits = set(clause) for v, sign in lits: if (v, not sign) in lits: return None return list(lits)

4.3 子句判据：CNF 里每个子句都含互补文字对

这里有一个非常漂亮的判据：一个 CNF 公式是重言式，当且仅当它的每一个子句都含有互补文字对。

理由不复杂。CNF 是若干子句的合取，合取为重言式当且仅当每个合取项都是重言式；而一个析取子句是重言式当且仅当它包含p ∨ ¬p这种形式，也就是含互补文字对。

def is_tautology_cnf(node): """等价推演路线：消蕴含 → NNF → CNF → 逐子句判互补""" nnf_node = to_nnf(eliminate_impl(node)) clauses = cnf_clauses(nnf_node) if not clauses: # 空合取，按理论是真 return True for c in clauses: if not any((v, not s) in set(c) for v, s in c): return False # 有子句不含互补对，整体非永真 return True

这里有个边界要留意：如果cnf_clauses返回空列表（理论上&节点为空时才会出现，正常输入不会），按定义空合取为真，返回True是合理的。真值表路线那边同样要处理空公式的情况，两边行为要一致，否则对拍时会莫名其妙报不一致。

4.4 两条路线的边界：什么时候枚举会死，什么时候推演会炸

没有哪条路线是万能的，选错会很难看。我用一张表把边界说清楚：

我的建议很简单：两套都实现，入口处按变量数和子句数上限做路由。变量数 ≤ 20 走真值表（顺便给反例和主范式），大于 20 走 CNF 判据，同时在 CNF 展开过程中设一个子句数上限（比如 10 万），超了就报「超出处理能力」而不是让程序跑到天荒地老。这个「双路线 + 路由」的设计在答辩时是很加分的，因为它说明你理解了两条路各自的边界，而不是只会背一个算法。

5. 避坑与排查：五个让程序当场翻车的现场

这一章是我改别人代码时反复遇到的五类问题，按「现象 → 原因 → 解决」写。每一条我都见过至少两次，其中前两条的危害最大，因为程序不会报错，只会安安静静地给出错误答案。

5.1 现象：!p & q被判成!(p&q)

现象：输入!p & q，当p=真, q=假时程序输出真；而手算!真 & 假 = 假。

原因：p_not在解析完!之后，调用的是p_and而不是p_atom，导致否定把整个合取式吞进去了。这在递归下降里非常常见，因为一层函数调错下一层不会报错，只是把树形改变了。

解决：p_not的递归调用必须是self.p_not()（处理连续否定）或self.p_atom()（处理原子），绝不能是任何二元层的函数。写完后用三个断言自检：!p & q应为('&', ('!', p), q)；!p | q应为('|', ('!', p), q)；!(p&q)应为('!', ('&', p, q))。这三个过不了，后面全白搭。

5.2 现象：主析取范式的最小项编号整体错位

现象：真值表里明明有 3 个为真的行，输出的主析取范式却编成了另外几个号；把公式的书写顺序换一下（p&q改成q&p），编号还会变。

原因：两处错误叠加。一是变量收集用了set直接迭代，没有排序，顺序随哈希变化；二是位序映射写成了(mask >> i) & 1而不是(mask >> (n-1-i)) & 1。

解决：collect_vars必须return sorted(out)；位序映射统一成高位对应前一个变量。再加一个自检用例：p | q在变量[p, q]下，最小项应为{1, 2, 3}（即!p&q、p&!q、p&q）。这个例子能同时验证排序和位序，写完就跑，跑不过别往下写。

5.3 现象：p | !p被判成非重言式

现象：输入p | !p，程序说不是重言式，甚至输出「变量数 0」。

原因：求值时用了 Python 的短路语义a or b，第一个操作数为真就直接返回，第二个分支里的变量p从来没被访问过；如果变量收集和求值写在同一个递归里，变量表就是空的，真值表只跑一次，结果取决于p的初始值。

解决：变量收集必须和求值彻底分离，先collect_vars走完整棵树，再进枚举循环。这条规则没有例外，别为了「省一次遍历」把两件事合并，省下的是毫秒，赔上的是正确性。另外，eval_node里不要用env.get(name, False)这种兜底写法，变量缺失就该抛KeyError，让问题暴露在还能定位的时候。

5.4 现象：长公式递归深度爆栈

现象：输入一个 2000 字符的公式，RecursionError: maximum recursion depth exceeded。

原因：eval_node和cnf_clauses都是纯递归，深度等于树的深度。像p1 & p2 & p3 & ... & p200这种左结合链，树退化成链表，深度就是 200，接近 Python 默认的 1000 上限；eliminate_impl里<->展开会让深度再翻倍。

解决：优先改数据结构而不是调sys.setrecursionlimit。求值可以改成显式栈的后序遍历，eval_node换成迭代版本，深度问题立刻消失。如果时间紧，退一步：在入口处限制公式长度上限（比如 1000 字符），超过就明确报错；同时在eliminate_impl之前先做一遍括号深度检查，深于 200 的直接拒绝。调递归上限只能当最后手段，调大了会撞 C 栈，报的是段错误，比RecursionError难查一百倍。

5.5 现象：CNF 展开时内存爆掉

现象：一个看起来不大的公式，跑cnf_clauses时内存一路涨到几个 G，最后被系统杀掉。

原因：|分支的[a + b for a in left for b in right]是笛卡尔积。多个|串联时子句数按乘积叠加，(a1&b1) | (a2&b2) | (a3&b3) | ...每加一项，子句数翻倍。

解决：三层防护。第一层，合并时立刻调用simplify_clause，子句里出现互补文字对就丢弃，这一条能砍掉大部分爆炸。第二层，设一个子句数上限（我一般用 50000），每次合并后检查len(clauses) > LIMIT，超了立即抛异常并回退到真值表路线。第三层，如果公式里|的嵌套层数超过 6，入口处就直接路由到真值表，不给它炸的机会。这三层加起来，实际能跑到爆炸的概率很低。

6. 从能跑到能交：对拍、用例清单和答辩会被追问的点

代码能跑通不等于能交。这一章讲怎么把「我相信它是对的」变成「我能证明它是对的」，顺便说说答辩时最容易被追问的地方。

6.1 随机公式对拍：让两种实现互为 oracle

两条路线（真值表和 CNF 判据）在理论上等价，这就是天然的验证工具。随机生成一批公式，两边都跑，结果不一致就打印出来人工分析。这比手写一百个用例有效得多。

import random def random_formula(depth, names): """随机生成语法树，depth 控制复杂度，防止无限递归""" if depth == 0 or random.random() < 0.3: v = random.choice(names) return ('var', v) if random.random() < 0.5 else ('!', ('var', v)) op = random.choice(['&', '|', '->', '<->']) return (op, random_formula(depth - 1, names), random_formula(depth - 1, names)) def cross_check(rounds=2000, names=('p', 'q', 'r', 's')): for k in range(rounds): f = random_formula(3, names) # 深度 3，变量 4 个，规模可控 a = all(v for _, v in truth_table(f)[1]) b = is_tautology_cnf(f) if a != b: print(f'不一致 #{k}: {f} 真值表={a} CNF={b}') return False print(f'{rounds} 轮对拍全部一致') return True

depth=3加上 30% 的叶子提前返回概率，生成的公式平均节点数在 15 左右，单次对拍在毫秒级，跑 2000 轮也就几秒钟。变量控制在 4 个以内，2^4=16 行真值表，不会拖慢速度。

如果对拍报出不一致，先别改代码，先把那个公式打印出来人工手算。绝大多数情况是 CNF 那条路线错了（真值表太简单，几乎不会错），而且集中在两处：eliminate_impl里<->展开的第二个合取项写反，或者to_nnf里neg传递时运算符翻转搞错。这是我见过最高频的两个 bug。

6.2 边界用例清单

对拍只能覆盖随机分布，边界还得靠手写。下面这张表建议直接做成测试文件，每条一个assert：

第 5 条值得单独说：(p->q)&(q->r)->(p->r)是假言三段论，恒真，但它的树形很深，蕴含右结合写错的话这条一定挂。第 7、8 条考察的是解析层，第 9 条考察错误提示——老师随手敲个错公式，你的程序报SyntaxError: 位置 4 出现无法识别的字符 '&'，和报一个空指针，观感完全不同。

6.3 答辩会被追问的三个点

第一个：「你这个程序变量多了会怎样？」这是在问复杂度意识。标准回答是给出具体数字：变量数 ≤ 20 走真值表，秒级；20～24 走真值表但会明显变慢，入口处提示；超过 24 自动切 CNF 判据，并对子句数设上限，超限报错而不是卡死。能说清楚「什么时候不行」，比说「我的程序很快」有说服力得多。

第二个：「你怎么保证结果是对的？」别答「我测了很多例子」。答对拍：两条独立实现的路线互相验证，2000 轮随机公式零不一致，加上 10 条边界用例覆盖解析层和求值层。有这套东西，老师基本不会再追。

第三个：「主析取范式的最小项编号怎么来的？」这题考的是你有没有真正理解编号规则，而不是抄了个公式。答：变量按字典序排定位置，真记 1、假记 0，高位对应靠前的变量，组成二进制转十进制，与教材定义一致；并且变量顺序在收集阶段就固定，不随书写顺序变化。

最后说一句我自己的习惯。写这类课设，我会先在纸上把真值表手算三行，再写代码，代码跑出来的第一件事就是对着那三行核对。这看起来笨，但它能在你还没开始调试算法之前就把解析层的错误拦下来。见过太多人算法写得很漂亮，结果卡在一个!p&q的优先级上耗掉整晚。希望帮到你。

本文还有配套的精品资源，点击获取