可满足性问题(satisfiability problem,简称SAT问题)作为第一个被证明的NP完全问题,有着重要的理论及应用意义。它是计算机理论与应用的核心问题,在计算机科学、人工智能等学科中有重要的理论及应用价值。而对可满足性问题求全解,在电子设计自动化(Electronic Design Automation,简称EDA)领域有着重要的应用价值。本文介绍了对可满足性问题求全解的理论及实践意义。对可满足性求解器算法进行比较,从中选择了效率较高且适用于全解求解器的算法。分别从增量式和隔离子句的角度,提出了两点适用于全解求解器的新算法:(1)从增量式角度对文字权值进行调整,并提出对隔离子句的冲突分析及回溯处理。本算法结合了布尔可满足性程序中的变量状态独立衰减总和的启发式决策算法,对于全解求解器运行过程中加入的隔离子句所涉及的文字权值进行调整,从而提高全解求解效率。对隔离子句造成的冲突提出专门的冲突分析及回溯处理机制,使每次添加一个隔离子句后,程序可以迅速进入下一次求解过程。(2)从隔离子句的角度对全解求解器进行改进。提出了基于CNF的类Don’tcares算法。这一算法借鉴了基于混合表示法(hybrid representations,即将电路特征和合取范式相结合)的Don’t cares算法,提出了单纯基于合取范式输入法的类Don’t cares算法。使基于CNF输入的全解求解器效率得到了一定程度的提高。提出对隔离子句的归并处理策略。能够对当前得到的隔离子句进行一定程度的归并处理,又不需要消耗太多的运行时间和系统空间资源。从实验结果可以看出以上两种算法对全解求解器效率的提高。