命题公式的可满足性问题（SAT问题）是判定是否存在一组变元真值赋值使得给定公式为真,MAX-SAT问题是SAT问题的最优化形式,寻找一组变元赋值使其满足的子句数最多。许多问题可以建模为SAT问题或MAX-SAT问题进行求解。冲突驱动子句学习算法（CDCL）和局部搜索算法（LS）是求解两类问题的重要算法。在实际算法验证中,通过调用合适的分支策略,可以提高CDCL算法性能;通过引入适当的翻转变元策略,可以提高LS算法的计算效率。本文主要研究SAT问题和MAX-SAT问题的改进算法,具体工作如下:（1）提出一种在CDCL框架中计算分支策略有效性的算法,算法基于搜索中学习子句的数量、质量和时间代价。设计动态调度分支策略算法,将求解过程分为两个阶段,在评估阶段计算分支策略的有效性,在非评估阶段,选择得分最高的分支策略进行求解。（2）提出一个新的变元选择策略——停时策略。LS算法中变元选择策略至关重要,高效的策略要尽可能避免局部最优。停时策略利用停时实现了变元选择策略的近似化,使得变元选择更加多元化,减少了局部最优现象。将停时策略引入经典的CCA求解器中,实验结果表明停时策略提升了求解器求解随机实例的性能。（3）分析了求解MAX-SAT问题时LS算法的变元选择策略,提出了一种基于不满足子句信息的变元选择策略,该策略不再从随机选择的一个不满足子句中挑选变元翻转,而是更多地考虑不满足子句的权值及得分信息,从最大得分或较优的不满足子句集中挑选变元翻转。实验结果表明此策略是有效的。