简介重言式判别程序课程设计资料包面向数据结构与算法学习者聚焦布尔表达式恒真性判定这一典型课程设计题目。内容围绕二叉树表示逻辑表达式、后序遍历求值以及栈辅助计算展开涉及与、或、非等运算符处理并延伸至用户输入交互、测试用例设计和文档撰写适合计算机相关专业学生完成同类课设或巩固树与栈应用时参考。压缩包共4个文件以2份doc文档和2份C源码为主文档覆盖项目概述、设计思路与算法说明C文件对应程序实现整体约38KB体积轻便便于查阅。已有383人学习下载说明该题目在课程设计中具有一定代表性。读者可从中获得重言式判别的完整实现框架包括表达式建树、遍历求值、栈操作和结果判断思路也能参考课程设计文档的组织方式与测试记录写法用于对照完善自己的方案或排查逻辑运算中的常见问题。1. 重言式判别程序一道被低估的数据结构课程设计命题逻辑里一个公式如果对变元的任意取值都为真它就叫重言式。数据结构课程设计里有个经典题目——重言式判别程序输入一串形如(P-Q)(Q-R)-(P-R)的式子程序要给出「是」或「不是」最好还能说清楚为什么不是。很多人第一反应是拿字符串函数糊一遍觉得无非是找找括号、数数符号真跑起来才发现问题全在细节里P-Q-R到底往哪边结合!PQ里那个感叹号管多长-被拆成三个字符之后整条链子就崩了。这份课程设计资料适合两类人正在赶数据结构课设、想拿栈和二叉树练手的同学以及想把「词法分析—语法分析—建树—求值」这条链路完整走一遍的开发者。它体量不大但词法、优先级、递归、回溯、内存释放一样不少是个能完整讲清楚的样本。2. 骨架先立住三层模块划分与工程目录结构2.1 为什么不能边读边算最朴素的写法是一边扫字符一边算结果遇到就把左右两边求出来。这种写法在只处理单个公式时勉强能跑一放到课设的验收场景就露馅验收通常要求一次读入文件里的几十条公式、逐条输出判定结果和真值表如果每次都重新扫描原串等于把解析成本乘上了公式长度。所以整条链路拆成三层各管一段词法层负责把字符流切成 token-是一个 token 而不是三个字符。语法层负责处理优先级与结合性把中缀序列变成后缀序列再由后缀序列自底向上建一棵表达式树。语义层只跟树打交道做真值枚举或者归约分支完全不需要知道原始字符串长什么样。这样分层的好处很直接词法层可以单独拿一堆畸形输入去测语法层可以打印后缀序列肉眼比对语义层可以手工构造一棵树来验证求值函数。三层里任何一层出问题定位范围都很小不用对着几百行 main 函数猜。表达式树还有一个隐性收益——共享。像(P-Q)(Q-P)这种式子同一棵子树在真值表枚举时会被反复访问 2^n 次字符串重扫是 O(长度)树上求值平均是 O(节点数) 且常数小得多。变量数上到 8 个以上时这个差距就很明显了。2.2 目录结构与构建方式课程设计资料的典型结构是这样源码、测试样例、文档三块分开交作业的时候文档直接对应报告章节tautology/ ├── src/ │ ├── main.c 主流程读参数、读输入、串起三层 │ ├── tokenizer.c/.h 词法扫描字符流 - Token 数组 │ ├── parser.c/.h 中缀转后缀、后缀建树 │ ├── tree.c/.h 结点创建、克隆、销毁、变量收集 │ ├── judge.c/.h 真值表法、归约分支法 │ └── report.c/.h 真值表打印、反例打印、范式输出 ├── tests/ │ ├── case01.txt 逐条公式一行一条 │ └── run_tests.sh 批量跑样例、比对期望输出 ├── docs/ │ ├── 需求分析.md │ ├── 概要设计.md │ ├── 详细设计.md │ ├── 测试用例.md │ └── 课程设计报告.docx ├── Makefile └── README.md本地跑起来就三步用 Makefile 比手敲 gcc 稳尤其是在加了-Wall -Wextra之后很多隐藏的类型问题会提前暴露make # 产物在 bin/tautology ./bin/tautology (P|!P) # 直接传公式判一条 ./bin/tautology -f tests/case01.txt # 按行读文件批量判 make test # 跑 tests/run_tests.sh 比对期望输出提示命令行参数里带!、、的单条公式一定要用引号包起来否则 shell 会先做历史展开或者重定向程序收到的是半截字符串报的错看起来像是词法分析写错了其实是 shell 干的。2.3 三个核心数据结构整个程序只有三个结构体撑着定义清楚之后后面所有代码都好写#define MAX_EXPR 512 /* 运算符种类顺序无所谓但 prec() 里要一一对上 */ typedef enum { OP_NOT, OP_AND, OP_OR, OP_IMP, OP_EQU } OpKind; /* 表达式树结点叶子和内部结点共用一套结构用 isLeaf 区分 */ typedef struct TreeNode { int isLeaf; /* 1 命题变元0 运算符 */ char var; /* 变元名如 P只有叶子有效 */ OpKind op; /* 运算符种类只有内部结点有效 */ struct TreeNode *left; struct TreeNode *right; /* 单目运算符 ! 只用 leftright 保持 NULL */ } TreeNode; /* 运算符栈存 OpKind 而不是字符省掉来回转换 */ typedef struct { OpKind data[MAX_EXPR]; int top; /* 空栈为 -1 */ } OpStack; /* 真值环境下标 变元字母 - A值取 0/1-1 表示未赋值 */ typedef int Env[26];Env用固定 26 长度数组而不是哈希表是因为课设里变元就是大写字母P、Q、R最多二十几个直接按下标寻址最快也免去了内存管理。真值表枚举时每个 mask 只需重写varCnt个位置其他位置留着旧值也不影响因为求值只会读树里出现过的变元。right指针在单目结点上留空是有意为之后面freeTree和cloneTree里都靠这个约定走轮到!的时候只递归左孩子。省一个children[]数组会让代码短不少代价是必须记住这个约定团队里换个人接手就得重新说一遍。3. 解析链路中缀转后缀再加一次建树3.1 词法扫描两字符运算符必须先于单字符匹配词法层的任务是把(P-Q)!R切成(、P、-、Q、)、、!、R八个 token。这里最容易被忽略的是匹配顺序-必须以整体出现如果把、-、当独立符号处理后面的语法层就彻底没法救了。同理-单独出现也算非法因为本项目只支持-。typedef enum { TK_VAR, TK_OP, TK_LP, TK_RP } TokenKind; typedef struct { TokenKind kind; char var; /* TK_VAR 时有效 */ OpKind op; /* TK_OP 时有效 */ } Token; /* 返回 token 个数出错返回 -1out 由调用方保证至少 max 个 */ int tokenize(const char *src, Token out[], int max) { int n 0; const char *p src; while (*p) { if (*p || *p \t || *p \r || *p \n) { p; continue; } if (n max) return -1; /* 超长直接失败别截断 */ if (*p A *p Z) { out[n].kind TK_VAR; out[n].var *p; n; } else if (*p () { out[n].kind TK_LP; p; } else if (*p )) { out[n].kind TK_RP; p; } else if (*p !) { out[n].kind TK_OP; out[n].op OP_NOT; n; p; } else if (*p ) { out[n].kind TK_OP; out[n].op OP_AND; n; p; } else if (*p |) { out[n].kind TK_OP; out[n].op OP_OR; n; p; } else if (*p - p[1] ) { /* - 两字符 */ out[n].kind TK_OP; out[n].op OP_IMP; n; p 2; } else if (*p p[1] - p[2] ) { /* - 三字符 */ out[n].kind TK_OP; out[n].op OP_EQU; n; p 3; } else { return -1; /* 非法字符交给上层报行号 */ } } return n; }这段代码里max参数不是摆设。课设的验收样例里经常出现几千字符的长公式固定 512 的栈数组一旦被写穿表现是程序在别的地方随机崩溃排查起来极其痛苦。让tokenize显式返回 -1上层打印「公式过长第 N 行」比事后用调试器找越界省事得多。另外注意p[1]、p[2]的读取C 字符串以\0结尾读到结尾之后p[1]已经越界了。严格写法是先判断p[1] ! \0实际工程里因为\0之后通常是分配器填充或者零页读一下不会崩但用 AddressSanitizer 跑一遍就会报出来。我在课设验收前都会用-fsanitizeaddress编一版跑全部样例。3.2 优先级与结合性调度场算法的两个开关中缀转后缀用的是经典的双栈思路简化版——只需要一个运算符栈。规则是读到变元直接输出读到左括号压栈读到右括号弹栈直到遇到左括号读到运算符时先把栈顶所有「优先级更高或同级且左结合」的运算符弹出去输出再把自己压进去。优先级和结合性决定了弹栈条件五个运算符的设定是运算符记号优先级结合性元数否定!5右单目合取4左双目析取|3左双目蕴含-2右双目等价-1右双目蕴含和等价设成右结合不是随便定的。数理逻辑里P-Q-R的通行约定是P-(Q-R)如果把-当左结合(P-Q)-R和P-(Q-R)在很多赋值下结果不同判定结论会直接反过来。这就是很多课设「样例能过、换条公式就错」的根源。static int prec(OpKind op) { switch (op) { case OP_NOT: return 5; case OP_AND: return 4; case OP_OR: return 3; case OP_IMP: return 2; case OP_EQU: return 1; } return 0; } /* 把中缀 token 序列转成后缀返回后缀长度出错返回 -1 */ int toPostfix(const Token in[], int n, Token out[]) { OpStack st; st.top -1; int k 0, paren 0; for (int i 0; i n; i) { if (in[i].kind TK_VAR) { out[k] in[i]; } else if (in[i].kind TK_LP) { st.data[st.top] OP_NOT; /* 占位用实际判断靠 in 的 kind */ paren; } else if (in[i].kind TK_RP) { /* 弹到左括号为止左括号本身丢弃 */ while (st.top 0 st.data[st.top] ! OP_NOT) out[k] mkOp(st.data[st.top--]); if (st.top 0) return -1; /* 括号不匹配 */ st.top--; paren--; } else { OpKind cur in[i].op; /* 单目 ! 和 - - 右结合同级不弹 */ int rightAssoc (cur ! OP_AND cur ! OP_OR); while (st.top 0 st.data[st.top] ! OP_NOT) { OpKind topOp st.data[st.top]; int topPrec prec(topOp), curPrec prec(cur); if (topPrec curPrec || (topPrec curPrec !rightAssoc)) { out[k] mkOp(topOp); st.top--; } else break; } st.data[st.top] cur; } } if (paren ! 0) return -1; /* 左括号多了 */ while (st.top 0) { if (st.data[st.top] OP_NOT) return -1; /* 残留占位 括号没配平 */ out[k] mkOp(st.data[st.top--]); } return k; }上面这段为了让左括号能压进OpKind栈借了OP_NOT当占位符写法上不太干净。真要交作业我更推荐把栈元素改成{int isLeftParen; OpKind op;}的小结构体或者干脆用int存-1表示左括号。占位符的写法虽然省两行但半年后回头看会想不起OP_NOT在这里代表什么属于自己给自己埋雷。mkOp是个几行的小工具函数负责把一个OpKind包成Tokenstatic Token mkOp(OpKind op) { Token t; t.kind TK_OP; t.var 0; t.op op; return t; }3.3 后缀建树先出栈的是右孩子有了后缀序列建树就变成一次自底向上的归约遇到变元就造一个叶子压栈遇到运算符就弹出操作数造一个内部结点再压回去。唯一需要刻在脑子里的规则是——先弹出的是右操作数。因为后缀里左操作数先出现、先入栈所以它在栈里位置更靠下后弹出。/* 由后缀序列建树成功返回根失败返回 NULL */ TreeNode *buildTree(const Token post[], int n) { TreeNode *stack[MAX_EXPR]; int top -1; for (int i 0; i n; i) { TreeNode *node (TreeNode *)calloc(1, sizeof(TreeNode)); if (!node) { freeStack(stack, top); return NULL; } if (post[i].kind TK_VAR) { node-isLeaf 1; node-var post[i].var; } else { node-isLeaf 0; node-op post[i].op; if (post[i].op OP_NOT) { if (top 0) { free(node); freeStack(stack, top); return NULL; } node-left stack[top--]; /* 单目只取一个 */ } else { if (top 1) { free(node); freeStack(stack, top); return NULL; } node-right stack[top--]; /* 先出栈的是右孩子 */ node-left stack[top--]; } } stack[top] node; } if (top ! 0) { freeStack(stack, top); return NULL; } /* 必须只剩一个根 */ return stack[0]; }那三个top检查看着啰嗦其实是防御式编程的核心。没有它们输入P这种残缺公式时stack[top--]会读到栈外内存拿到一个随机指针塞进node-right然后求值阶段访问野指针直接段错误。加了检查之后程序能稳定输出「公式语法错误」。验收老师一般不会因为程序报错扣分但一定会因为崩溃扣分。freeStack在失败路径上负责把栈里已经建好的子树全部释放避免半成品泄漏。这个函数本身只有五行容易被漏写写完记得在 ASan 下把每个错误分支都跑一遍。4. 判别引擎真值表枚举与归约分支两条路4.1 变量收集与真值表枚举真值表法的思路没什么花哨先找出公式里出现了哪些变元n 个变元就有 2^n 种赋值逐个代入求值只要撞上一组让它为假的赋值就说明不是重言式顺手把这组反例打出来。/* 中序遍历收集变元去掉重复结果按字母序排好方便打印 */ void collectVars(const TreeNode *t, int seen[26], char vars[], int *cnt) { if (!t) return; if (t-isLeaf) { int idx t-var - A; if (!seen[idx]) { seen[idx] 1; vars[(*cnt)] t-var; } return; } collectVars(t-left, seen, vars, cnt); collectVars(t-right, seen, vars, cnt); } /* 按 env 求值返回 0/1 */ int evalTree(const TreeNode *t, const int env[26]) { if (!t) return 0; /* 兜底正常不会走到 */ if (t-isLeaf) return env[t-var - A] ? 1 : 0; switch (t-op) { case OP_NOT: return !evalTree(t-left, env); case OP_AND: return evalTree(t-left, env) evalTree(t-right, env); case OP_OR: return evalTree(t-left, env) || evalTree(t-right, env); case OP_IMP: return !evalTree(t-left, env) || evalTree(t-right, env); case OP_EQU: return evalTree(t-left, env) evalTree(t-right, env); } return 0; } /* 返回 1 重言式0 不是并打印反例-1 变元过多 */ int judgeByTable(const TreeNode *root, int verbose) { char vars[26]; int seen[26] {0}; int varCnt 0; Env env; collectVars(root, seen, vars, varCnt); sortVars(vars, varCnt); /* 插入排序即可最多 26 个 */ if (varCnt 16) return -1; /* 65536 次枚举是上限再多就跑不动了 */ int total 1 varCnt; for (int mask 0; mask total; mask) { for (int i 0; i varCnt; i) env[vars[i] - A] (mask (varCnt - 1 - i)) 1; if (!evalTree(root, env)) { if (verbose) printCounterExample(vars, varCnt, env); return 0; /* 见假即停省一大半时间 */ } } return 1; }几个细节值得说。sortVars用插入排序不是偷懒26 个元素以内插入排序比qsort快且不用函数指针打印出来的真值表列序也稳定。mask (varCnt - 1 - i)的意思是把最高位对到第一个变元这样打印真值表时从000到111是自然顺序人眼扫起来顺。varCnt 16的硬阈值是血泪得来的。课设里变元一般不超过 5 个但有人会把P|!P这种恒真式当测试样例批量塞进文件如果每条都展开 2^20 次枚举整个程序会卡住几十秒看起来像死循环。给个上限并提示「变元过多建议用归约法」比让它无声无息地跑下去体面得多。和||的短路特性在这里没有副作用因为求值是纯函数不会修改任何状态。但如果后面想扩展成「统计每个子式被求值的次数」这种带副作用的诊断功能就得改成先把左右都算出来再合并否则统计出来的数字会明显偏小。4.2 归约法先消去蕴含等价再做分支回溯真值表法是最笨也最可靠的路子规模一大就废。归约法的思路是先把公式改写成只含!、、|的等价形式再对析取做分支、对合取做合并走不通就回溯。判断重言式用的是反证把公式取反看它是否可满足不可满足就说明原式恒真。改写规则就两条A - B等价于!A | BA - B等价于(A B) | (!A !B)/* 递归消去 - 和 -返回改写后的树会就地修改并克隆子树 */ TreeNode *eliminate(TreeNode *t) { if (!t || t-isLeaf) return t; t-left eliminate(t-left); t-right eliminate(t-right); if (t-op OP_IMP) { /* A - B !A | B */ TreeNode *notA makeNot(t-left); t-op OP_OR; t-left notA; } else if (t-op OP_EQU) { /* A - B (A B) | (!A !B)两边都要深拷贝 */ TreeNode *pos makeAnd(cloneTree(t-left), cloneTree(t-right)); TreeNode *neg makeAnd(makeNot(cloneTree(t-left)), makeNot(cloneTree(t-right))); t-op OP_OR; t-left pos; t-right neg; } return t; }cloneTree是这里的必需品不是可选项。-改写之后原来的左右子树要在新树里出现两次如果直接复用指针就变成了一棵有共享子树的图后面freeTree递归释放时同一块内存会被释放两遍程序在退出那一刻崩溃而这个现象跟判定逻辑毫无关系能让人怀疑人生。深拷贝一次代价可控公式规模就那么大。改写完成之后做分支。这里用一个-1/0/1的三态环境记录每个变元的赋值-1未定、0假、1真。遇到析取就左右各试一次遇到合取就两边都必须成立碰到变元或它的否定就尝试赋值冲突即回溯。/* 判断 f 在 env 下是否可满足可满足返回 1env 里留下那组赋值 */ int sat(const TreeNode *f, int env[26]) { if (!f) return 1; if (f-isLeaf) { int idx f-var - A; if (env[idx] -1) { env[idx] 1; return 1; } return env[idx] 1; } if (f-op OP_NOT) { /* 叶子取反 */ if (f-left f-left-isLeaf) { int idx f-left-var - A; if (env[idx] -1) { env[idx] 0; return 1; } return env[idx] 0; } return 0; /* 改写后不应出现非叶子的 ! */ } if (f-op OP_OR) { int backup[26]; memcpy(backup, env, sizeof backup); if (sat(f-left, env)) return 1; /* 左支成功就结束 */ memcpy(env, backup, sizeof backup); /* 左支失败回滚 */ return sat(f-right, env); } if (f-op OP_AND) { int backup[26]; memcpy(backup, env, sizeof backup); if (sat(f-left, env) sat(f-right, env)) return 1; memcpy(env, backup, sizeof backup); return 0; } return 0; }回滚那两行是这个函数里最关键的代码也是最容易漏的。漏掉之后左支尝试失败留下的半截赋值会污染右支的判断表现是某些本该判为重言式的公式被判成不是——而且只在含三个以上变元、两次改写分支的公式上才复现样例测试根本抓不到。判定入口就是把原树取反再问一次int judgeByReduce(TreeNode *root, int verbose) { TreeNode *f eliminate(cloneTree(root)); /* 不动原树方便切回真值表法 */ TreeNode *neg makeNot(f); int env[26]; for (int i 0; i 26; i) env[i] -1; int s sat(neg, env); /* 取反后不可满足 原式是重言式 */ if (s verbose) printCounterExample(env, 26); freeTree(f); freeTree(neg); return !s; }4.3 两种方法的取舍两条路各有各的适用面实际工程里通常是「小规模用真值表给反例大规模用归约省时间」维度真值表法归约分支法时间复杂度固定O(2^n * 节点数)与公式形状无关最坏仍是指数但平均远快于枚举能否给出反例天然能撞到假值即得能回溯找到的赋值就是反例实现难度低一个循环加一个递归求值中改写和回溯都要处理内存变元数上限16 个左右再多不可接受20 个以内通常能跑出错风险主要错在枚举位序主要错在回溯没恢复环境课设验收通常要求两种都实现并且对同一批样例输出一致的结果。这个要求看着像凑工作量实际是给你一个交叉验证的抓手——两套完全不同的代码路径给出同一个答案逻辑写错的概率就低得多。5. 避坑与排查五处让结果静默出错的地方这章记的是我在改这份课设时真踩过的坑。它们共同的特点是程序不崩、结果不对比直接段错误难查十倍。5.1 解析与建树阶段的三处陷阱坑一-被拆成了三个符号现象是含等价的公式一律被判成语法错误而只含-的公式全部正常。原因是词法扫描里-的分支写在了-分支前面指针先匹配到时走了非法字符分支。解决办法是把多字符运算符的判断放在单字符之前并且严格按长度从长到短排先试-三个字符再试-两个字符最后才是单个符号。这个顺序一旦反了-永远匹配不上。坑二单目!的作用范围算错输入!PQ人读是(!P)Q但程序算成了!(PQ)。根本原因是把!当成了普通的双目运算符处理建树时给它弹了两个操作数。修法是两点prec(OP_NOT)给最高优先级保证它一进栈就不会被别的运算符压住建树时对单目单独走一条只弹一个孩子的分支。同理!!P也要能正确建出两层否定这要求!之间不能互相弹出。坑三建树时左右孩子接反这是最阴的一个。P-Q和Q-P在左右接反的代码里会得到一模一样的树所以测试P-P恒真能过测试(P-Q)|(Q-P)恒真也能过直到测到(P-Q)-(Q-P)才发现结果不对。定位方法很简单写一个printInfix(root)把树按中缀打印出来跟原式逐字符比对。从那以后我养成习惯建树函数写完第一件事就是打印回原式确认往返一致再往下写。5.2 求值与资源管理阶段的两处陷阱坑四真值表枚举的位序与打印列序不一致程序判定「不是重言式」打印出来的反例赋值抄进公式一算却是真。原因是枚举时用mask (1 i)取位打印时却按vars[0]到vars[n-1]的顺序输出两边的位序一个从低到高、一个从高到低刚好镜像。这类错误不会让程序崩溃只会让所有反例看起来都是错的很容易被误判成求值函数写错。统一成「最高位对应第一个变元」之后就没再出过问题。坑五归约回溯时忘了恢复环境前面sat函数里那两行memcpy就是为此存在的。漏掉之后左分支失败的残留赋值会让右分支的变元被判成冲突公式被误判成不可满足于是一个非重言式被报成重言式。它的隐蔽性在于变元只有一两个时几乎不触发三个以上、公式里有嵌套析取时才冒头。排查手段是在sat入口打印当前env快照肉眼就能看到不该有值的位置被填了。5.3 一个能省下大量时间的排查顺序遇到结果不对别急着读求值函数按这个顺序走一遍通常五分钟内能定位打印 token 序列确认词法层切分正确尤其是多字符运算符和变元边界。打印后缀序列确认优先级和结合性没搞反P-Q-R的后缀应该是P Q R - -。用printInfix把树还原成中缀跟输入逐字符比对。手工构造一棵最简单的树比如只有P!P单独调evalTree排除求值层。最后才怀疑枚举位序和回溯环境。用-Wall -Wextra -fsanitizeaddress,undefined编一版跑全部样例越界和悬垂指针会当场被抓出来比事后猜测高效得多。6. 二次开发把课设改成能拿得出手的项目课设交完就扔太可惜这套「词法—语法—树—求值」的骨架稍微改改就能撑起不少东西。我按改造成本从低到高列了几个方向都是能在一两天内落地的改造方向主要改动点工作量风险点扩充运算符加异或^、与非、常量T/F半天优先级表要重排^通常给 3.5 级不好放干脆重编号输出主析取/主合取范式在真值表基础上收集成真行一天变元多时字符串会极长得加截断随机公式自测生成随机树两套判定交叉比对一天生成器要保证语法合法否则测的是解析器换 DPLL 或 BDD替换sat内核两到三天接口要重设计Env的语义得改第一个方向最划算。加异或之后prec表要重新编号别在原值中间插小数直接把五个运算符重排成 1 到 6改一处就够。加常量T和F更简单词法层把它们当变元处理然后在collectVars里跳过、evalTree里直接返回固定值树的结构完全不用动。第二个方向是课设报告里最容易出彩的部分。主析取范式就是真值表里所有成真行对应的极小项析取起来实现上不需要额外的树操作直接复用judgeByTable的枚举循环把evalTree返回 1 的 mask 记下来最后拼字符串/* 在枚举循环里收集成真行返回成真行数 */ int collectModels(const TreeNode *root, char vars[], int varCnt, int models[], int max) { Env env; int cnt 0; for (int mask 0; mask (1 varCnt) cnt max; mask) { for (int i 0; i varCnt; i) env[vars[i] - A] (mask (varCnt - 1 - i)) 1; if (evalTree(root, env)) models[cnt] mask; /* 记下成真赋值 */ } return cnt; }models数组长度是 2^varCnt调用前必须先判断变元数超过 12 个就别开了否则光这个数组就能吃掉几兆。拼极小项时注意某变元在 mask 对应位为 1 就写P为 0 就写!P项与项之间用|连接。如果成真行数是 0说明是矛盾式主析取范式按约定写F如果成真行数等于总数是重言式按约定写T——这两个边界不处理输出会变成空字符串看起来像程序没跑。第三个方向看着像锦上添花实际是投入产出比最高的。写一个随机公式生成器从给定的变元集合里随机挑运算符和子树拼装深度控制在 4 层以内然后分别交给真值表法和归约法判一遍两边结论不一致就直接把公式打印出来。我用这个办法在一个下午里揪出了三个手工样例永远碰不到的回溯 bug——它们只在特定形状的嵌套析取下才触发。生成器本身要保证语法合法别让它生成PQ这种非法串否则测的是解析器容错不是判定逻辑。第四个方向是真正拉开差距的地方。真值表法在 16 个变元以上就废了归约法在构造得很坏的公式上也会指数爆炸要往上走就得换内核。DPLL 的核心是三件事单元传播只有一个未赋值文字的子句直接定值、纯文字消去某变元在所有子句里只以一种极性出现就直接赋值、以及带监视文字的冲突分析。把sat函数替换成 DPLL外层接口judgeByReduce一行都不用改因为「取反后不可满足」这个判定语义是稳定的。这就是当初把判定逻辑和数据结构分开的回报。真正动手改的时候我建议先别急着加功能先把现有代码的测试补齐。课设的样例通常只有十来条覆盖不到P-Q-R的右结合、!!P的嵌套否定、-的深拷贝这几处高危路径。补测试的过程本身就是重新读一遍代码往往补到一半就发现问题了。我第一次交这份课设的时候判定结果在(P-Q)(Q-R)-(P-R)上是对的换了个(P-Q)-(P-Q)(Q-P)就翻车查了三小时才发现是-改写时没深拷贝两棵子树共享了同一个指针。从那以后我每次写这种带树结构改写的程序都强制先用 ASan 把全部样例跑一遍再手工构造三个共享子树的用例专门验证释放路径。希望这些踩过的坑能帮你少走一段弯路。本文还有配套的精品资源点击获取
