极小模型的计算在人工智能推理系统中是一项必不可少的任务。然而,即使是正CNF（Conjunctive Normal Form）公式,其极小模型的计算和验证都是不易处理的。当前,计算CNF公式极小模型的主要方法之一是通过将CNF公式转换为析取逻辑程序后,用回答集程序（Answer Set Programming,ASP）求解器计算其稳定模型/回答集。针对计算CNF公式的极小模型这一问题,本文提出了几个新方法,并将极小模型的求解应用到诊断问题中。本文具体工作如下:1)首先,提出一种基于SAT求解器的计算极小模型的方法MMSAT1;其次,结合最近基于极小规约的极小模型验证算法Check Min MR,提出了基于极小模型分解的计算极小模型方法MRSAT;然后根据极小规约的定义,结合算法MMSAT和MRSAT得到基于极小规约的算法MR＿MMSAT和MR＿MRSAT;最后,对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试实例进行测试。实验结果表明,本文提出的四种计算极小模型的新方法对随机3CNF公式和SAT工业测试实例都是非常有效的,且计算极小模型的速度都明显快于最新版的clingo。在SAT工业实例上发现了clingo5.4有计算出错的情况,而本文提出的方法则更稳定。2)将极小模型求解方法应用到基于模型的诊断（Model-Based Diagnosis,MBD）问题中。首先,提出基于极小模型求解方法MMSAT的计算组合电路极小诊断的新方法MMSAT＿Diagnosis和基于SAT求解器的新方法SAT＿Diagnosis。其次,提出一个诊断极小性判定定理并给出了完整的证明。最后在国际标准测试电路ISCAS-85上进行了测试。实验结果表明,本文提出的两种计算组合电路极小诊断的新方法都是非常有效的。本文算法实现代码及数据地址见GitHub2。