简介这份课程设计资料围绕重言式判别程序展开面向正在学习数据结构与算法、需要完成逻辑表达式相关课设的高校学生。内容以布尔表达式为对象讲解如何用二叉树组织变量及与、或、非等运算符并借助后序遍历和栈完成表达式求值从而判断其是否为恒真式同时涉及自定义表达式输入、测试用例设计与课程设计文档编写适合作为课设参考和算法综合练习。压缩包共4个文件包含2份doc设计文档和2份C语言源码整体约38KB文档用于梳理设计思路、算法描述与测试结果源码便于对照实现细节。目前已有383人学习读者可从中获得二叉树建树、遍历求值、栈辅助计算、交互设计与文档组织的完整参考。1. 重言式判别程序课程设计一行题目背后藏着三个判定引擎题目发下来只有一句话编程判断任意给定的命题公式是不是重言式。重言式判别程序课程设计看上去像一次词法分析练习——读字符串、建树、求值三步走完。真动手才发现卡住人的从来不是解析而是判定这一步该怎么收场。五个变元手算真值表还能撑住十个变元就是 1024 行二十个变元是 104 万行靠人眼对数早就崩了。这个题目的价值在于它逼着你在两条完全不同的路里做选择一条是老老实实枚举所有赋值另一条是把「恒真」翻译成「否定式不可满足」再用归结去反驳。前者好写但会撞上天花板后者聪明但会撞上子句爆炸。课程设计真正要交的不是一段能跑通的代码而是你能说清楚这两条路各自在哪里失效、边界参数怎么定。下面按我实际写过的顺序拆先做解析再做真值表引擎再做归结引擎最后用随机公式互相对拍。2. 从字符串到语法树把 ¬ ∧ ∨ → ↔ 拆成能给程序吃的 token命题公式在纸面上是二维的程序里必须先压成一维。这一步的产出是一棵语法树后面的两个判定引擎都只认这棵树不认原始字符串——这个约束很关键它保证了解析只写一次判定逻辑可以换着写。很多人图省事在求值函数里直接扫字符串写着写着就发现真值表引擎和归结引擎各自长出了一套解析代码改一个优先级要改两处血泪经验。2.1 优先级和结合性先钉死再谈代码命题逻辑的五个联结词有公认的优先级麻烦在于「太熟了反而容易写错」。¬ 最高依次是 ∧、∨、→↔ 最低。结合性更容易翻车∧ 和 ∨ 左结合→ 右结合也就是说p→q→r必须解析成p→(q→r)而不是(p→q)→r。这两个式子不等价前者在 p 假时恒真后者不是。联结词可接受的输入写法结合性优先级¬¬!~前缀右结合1最高∧∧左结合2∨∨|左结合3→→-右结合4↔↔-左结合5最低允许一个联结词有多种写法不是为了炫技是因为输入来源太杂教材用¬键盘上顺手敲!从别处复制过来的公式可能是-。词法层把它们归一到同一个 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 tokenstokenize里最容易忽略的是for...elsebreak只在匹配成功时走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, accNone): 递归收集所有命题变元返回按字典序排好的列表。 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∨BA↔B等价于两者真值相等。这两行如果图快写成evaluate(A) evaluate(B)在布尔值上恰好也对但只要中间插入任何非布尔的中间结果就会炸属于能跑但不该跑的写法。and和or那两行之所以快是因为 Python 的and/or是惰性求值左边为假and右边的evaluate根本不会被调用整棵子树被跳过。一次局部剪枝看起来微不足道在 2^20 行的循环里累计起来就是一倍以上的差距。3.2 短路求值加提前退出一行反例就够判非重言式判重言式和打印真值表是两件互相冲突的事。打印要求把 2^n 行全部列出来一行都不能少判别只要求找到一个使公式为假的赋值找到就能收工。课程设计常常两个要求一起提很多人就写成「先枚举全部再检查」白白丢掉了提前退出的机会。def is_tautology_truth_table(node, limit24): 返回 (是否重言式, 反例赋值)。找到反例立即返回不遍历全表。 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, Nonemask i 1这一句从低位往高位取配合vs的排序保证第 i 个变量对应第 i 个 bit。这个对应关系必须和打印真值表时用的一致否则人工核对时会发现「程序说 p 真 q 假表里却是 p 假 q 真」——不是算错是对齐反了。提前退出带来的加速不是线性的是指数级的量级差异被压成常数。构造一个p ∧ q ∧ r ∧ ...那种合取式第一个赋值全假就使整个公式为假程序第一轮直接返回。反过来如果公式确实是重言式就没有任何捷径2^n 行必须走满。所以真值表引擎的耗时上限只在「是重言式」这一侧被真正触发。要做完整的真值表打印就再写一个平行函数循环体里把env和evaluate的结果攒进列表最后统一格式化输出。两个函数共享collect_vars和evaluate只是外层循环的收尾条件不同。不要试图用一个early_exitTrue参数把两者揉在一起那个参数会传染到每一行读起来比写两遍更累。3.3 真值表法画出的边界n 到多少就该换引擎把复杂度摊开算一遍边界自然就出来了。设公式语法树的节点数为 k单行求值最坏 O(k)总复杂度 O(k·2^n)。实际代码里常数因子大概在几十纳秒的量级但决定性的还是那个 2^n。变元数 n赋值行数 2^n单行求值节点数 k估最坏求值次数8256约 205×10³124,096约 251×10⁵1665,536约 302×10⁶201,048,576约 404×10⁷2416,777,216约 508×10⁸n20 那一行是分水岭几千万次求值解释型语言跑起来要几秒到十几秒还在可接受范围n24 直接上到十亿量级程序会卡到让人以为死循环。所以我把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, negFalse): 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ⁿ 个子句n20 时就是一百万条子句内存直接爆掉。递归里的to_cnf被重复调用了两次同一个子树算两遍也让实际耗时比理论值更难看。真要在这种输入上跑正确的做法是换 Tseitin 编码给每个子公式引入一个辅助变元把它「当且仅当」原公式写成几条子句整个过程是线性的代价是变元数增加。Tseitin 不保持逻辑等价但保持可满足性等价而归结法只需要可满足性所以完全够用。课程设计如果不强制要求「只用原变元」这是值得主动加进去的加分项。4.2 子句集与归结式frozenset 去重加包含消除走到 CNF 之后把它拆成子句集。与节点递归下去或节点这边把整条链上的文字收成一个集合。文字用带符号的字符串表示正文字是p负文字是-p。这样判断互补只要拼一个减号比维护(name, sign)元组省事。def literals(node, signTrue, outNone): 把一条 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, accNone): 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 accfrozenset这个选择是强迫的内部子句要用哈希去重普通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 Noneresolve只返回第一个找到的归结式而不是所有可能的。严格说两个子句可能有多对互补文字应该产生多个归结式。实践里只取一个也够用——因为只要子句集最终饱和漏掉的那几个归结式总会在别的配对里被补出来。这个取舍能省掉大量重复子句是让程序能跑完的关键。4.3 饱和归结什么时候停空子句、无新子句、规模上限主循环是一个饱和过程每轮把当前子句集两两归结产生的新子句加进去直到某种终止条件触发。def is_tautology_resolution(node, max_clauses20000): 归结反驳¬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 hrefhttps://download.csdn.net/download/songkaisong/1326707 stylecolor:#ec7500;font-size:14px; 本文还有配套的精品资源点击获取 /a img altmenu-r.4af5f7ec.gif srchttps://csdnimg.cn/release/wenkucmsfe/public/img/menu-r.4af5f7ec.gif stylewidth:16px;margin-left:4px;vertical-align:text-bottom;cursor:text; /p
