改进Max-SAT算法的关键技术研究

SAT问题是理论计算机科学和人工智能领域中的基本问题. Max-SAT问题是SAT问题的一个很自然的扩展. 统计物理、生物信息学等领域中的许多问题都可以转化为Max-SAT问题. 近五年，Max-SAT求解的研究吸引了越来越多学者的关注. 每年举行的国际Max-SAT求解评比见证和推动了这一领域研究的发展. 申请人在2007年提出了分支定界算法中新的下界计算方法，基于这一方法的Max-SAT求解器Inc(W)Maxsatz在2008年的Max-SAT评比中表现优异. 在已有工作的基础上，本项目将研究如何将SAT求解中采用的two watched literals和clause learning技术结合进Max-SAT中求解中，研究将Max-SAT实例转化为SAT实例之后公式所具有的结构特性，研究适用于Max-SAT的局部搜索算法，以求进一步改进当前Max-SAT求解器的效率.

Max-SAT问题是经典的NP难问题，很多理论计算机科学和人工智能领域的问题都可以转化为Max-SAT问题，从而用Max-SAT求解器求解. 本项目主要有两个研究目标：其一是改进已有的Max-SAT算法和求解器；其二是借鉴Max-SAT算法，将其计算下界的方法用于求解其它NP难问题. 总体来讲，第一个目标的完成情况不如预期，虽然在2010年和2011年的国际Max-SAT求解评比中，我们的求解工具性能提升，依旧能获得不少奖项，但算法方面并无重要突破；针对第二个目标，我们将Max-SAT求解策略运用于求解最大团问题和最长公共子序列问题，后者的效果明显.