目前,现代工业人造系统的规模和功能越来越强大,同时系统的行为也变得越来越复杂。如果发生系统故障,不能及时有效的排除,就极有可能造成无法挽回的后果。可见,及时有效的诊断出系统故障并予以排除是非常重要的。近些年,国内外学者提出了多种故障诊断方法来对系统进行诊断,离散事件系统(Discrete Event System, DES)由于能够容易表征人造系统,所以基于DES的故障诊断方法是目前较热门的研究领域。命题可满足问题(satisfiability problem, SAT)是人工智能领域中的核心问题,也是解决许多实际问题的基础。目前针对SAT的求解算法已经非常高效,利用SAT求解的高效性来进行故障诊断是一个很好的课题。本论文归纳总结了故障诊断技术的研究进展,根据SAT求解算法的高效性的特点,将SAT求解算法运用到故障诊断中。具体地说,本文根据将待诊断的系统模型编码成SAT求解器能识别的格式,然后用SAT求解器进行求解,得出求解结果就是诊断结果,由于求解的结果是一组赋值,所以需要有一个解码(解释)的过程来将赋值转化为可读的诊断结果。本论文根据这种基于命题可满足的DES故障诊断技术,设计并实现一个支持该方法的故障诊断系统,利用SAT求解器进行故障诊断。为了检查本文的方法和对应的系统的运行效果,本文使用状态机自动生成算法米自动产生实验所需的状态机模型,并分析该诊断方法的诊断特性。实验表明,该故障诊断技术相对其它技术具有更好的诊断效果,证明该诊断系统具有一定的实用价值。