图G=(V,E)的一个树分解是将结点集V的子集作为树T的节点,使得在树T上任意一条路径的两个端节点之间的交集包含于该路径上的任意一个节点中,T上最小(节点)对应子集的元素个数减1定义为分解树的宽度,而图G的树宽是指所有分解树中宽度最小的值。一个合取范式(CNF)公式可以用一个二分图G=(VèC,E)表示(公式的因子图),其中变元结点集C对应为公式F中的变元集,子句结点集对应为公式中的子句集,变元在子句中的正(负)出现用实(虚)边表示。忽略公式因子图中边上的符号,得到一个二分图。在实际应用中,很多难解问题限制在小树宽下可以得以有效解决,甚至可以在多项式时间内进行求解。本文围绕该问题,基于一般图的树分解算法,提出了一种二分图的树分解算法,探索了CNF公式因子图的树宽与公式求解难度之间的联系。进一步,基于树分解这个工具来探究线性CNF公式及其对应的线性二分图,研究结果表明线性CNF公式具有良好的树宽上界。主要的研究成果如下:(1)基于一般无向图的树分解算法,提出了一种求解CNF公式关联的因子图的树分解算法。实验结果表明,随着CNF公式中子句约束密度的增大,公式因子图的树宽远小于变元规模,为进一步探究难解实例奠定了实验基础。同时,通过实验对比,验证了本文提出的二分图的树分解算法与另外三种经典的树分解算法相比,能够求解出更优的树宽。(2)基于线性CNF公式类,通过实验研究分析了线性二分图的树分解及树宽,进一步探究在小树宽的条件下CNF公式类的结构特征。研究表明,线性CNF公式类的树宽上界与公式本身的性质有着密切的联系,即当公式中任意两个子句之间的公共变元个数小于等于1时,线性CNF公式类的树宽小于等于变元在公式中出现的最大次数。实验结果表明,线性CNF公式的树宽上界小于等于非线性CNF公式的树宽上界。