可满足性问题(即SAT问题)是第一个被证明的经典NP问题。人们一直致力于如何在有限的时间求解可满足性问题。随着现实世界中可满足性问题的规模逐渐增长,预处理技术已经逐渐受到重视。由于其良好的简化效果,变量消除算法已经应用于多种预处理器中。作为一种轻量级预处理技术,变量消除算法的简化效果与其消除过程中的约束条件有着直接联系。为了进一步提高和优化变量消除算法的预处理性能,本文对比研究了在不同的约束条件下变量消除算法的简化性能以及简化后的CNF实例的求解效果,同时设计了一种基于子句文字长度动态约束的变量消除算法。与分解前的子句文字长度相比,只有当分解后的子句集合的文字长度减少时,该算法完成变量消除替换过程。为了减少变量消除算法中无价值计算,该算法引入了动态约束机制,大大缩短了预处理时间,进一步提高简化性能。本文在该算法的基础上,基于Mini Sat的开源代码实现了一个可满足性问题的预处理器MiniSat BFS。除了通过常规的性能指标来对比分析两种不同约束条件下变量消除算法的预处理性能。本文利用复杂网络的统计分析方法,将CNF实例转化为复杂网络表示,从复杂网络的整体和局部两个维度来分析简化前后的CNF实例,评估现有预处理算法的简化性能。最终的实验结果表明,与现有的基于子句数目约束的算法相比,新的算法不仅降低了CNF实例的规模,而且缩短了预处理过程和求解过程的时间消耗。更重要的是,改进后的算法在限定的时间内可以求解更多的可满足性问题,具备显著的性能优势。