SAT是最著名的NPC问题。NPC类问题有两方面的特性,首先,这类问题的解可以在多项式时间复杂度内得到验证。其次,其它NP问题可以在多项式时间内转换为NPC问题来求解。因此,SAT判定技术的研究具有重要的理论意义。SAT判定技术还具有很大的实用价值。它可以应用到包括人工智能规划、模型分析、定理证明、软件验证和软件测试、软件发布中的包管理等领域。在电子设计自动化中,SAT可用于电路的逻辑综合、布尔匹配、电路等价性验证、模型检验、自动测试用例生成、FPGA的布局布线、设计调试与诊断等。本文研究SAT判定问题,SAT判定问题的时间复杂度是指数阶的,这意味着如果问题的规模较大时,要完成SAT判定会非常困难。研究利用分治的思想,通过将复杂的SAT的判定问题划分为多个规模更小的子问题来求解,在划分代价较小的情况下,利用这一方法来降低可满足性判定的复杂度。通过系统深入的理论分析和实验研究,取得了如下创新性成果:提出了CNF形式的布尔公式的子句组划分的概念,并证明了布尔公式的可满足性问题可以转化为子句组的可满足性问题来求解。给出了一种从CNF公式产生子句组划分,以及利用子句组划分来进行SAT判定的方法。对于不能直接产生子句组划分的公式,提出利用聚类方法,将子句聚类成多个簇,把包含共同变量多的子句聚类到同一个簇,包含共同变量少的子句聚类到不同的簇,将不同簇之间的共同变量作为割变量,通过对每个簇单独判定,必要时再判断割变量的取值是否冲突来判定公式的可满足性。由于传统的聚类方法并不能很好地适应CNF子句的聚类要求,因此本文针对CNF公式的特点,提出一种两阶段的聚类方法,先用基于连接的方法来产生初始聚类,在一定程上避免聚类的局部最优性,然后再用基于簇间相似度进行合并的方法来生成最终的聚类结果。算法的第一阶段通过指定聚类结果簇与原始簇个数的比值来确定生成的簇的个数,第二阶段则通过相似度阈值来确定何时终止聚类,因此无需指定最终生成的簇的个数。在聚类完成之后,如果要消去所有簇之间的共同变量,将所有的簇都划分开,在某些情况下,由于公共变量太多,可能需要付出太大的代价。为解决这一问题,本文提出将聚类结果中的簇作为顶点,用簇间的公共变量来标记边,将聚类结果变换成一个无向图,然后利用无向图最小割的方法来寻找将簇划分成两组的最小割变量集,以产生子句组划分。在某些情况下,将问题变换为CNF公式,可能会导致一些结构信息的丢失。针对组合电路的等价性验证问题和AIG电路的特点,本文提出一种方法,直接在电路上通过电路的特点进行推理来判定Miter电路的可满足性,从而充分利用应用领域知识来提高AIG电路的可满足性判定效率。