求解SAT问题的线性半定规划算法
李厚银1
许道云2
万武族2
1.贵州大学理学院数学系,贵阳,5500252.贵州大学计算机科学系,贵阳,550025
摘要：将线性半定规划应用到SAT问题的求解过程中.首先将SAT实例转化为整数规划问题,然后松弛为线性规划模型,最后再转化为一般的线性半定规划模型去求解.用SDPA-M软件求解线性半定规划问题后,规定了如何根据目标函数值去判定SAT实例和当CNF公式可满足时如何根据最优指派的概率x*i(i=1,…,n)去进行变元赋值,以期求得该公式的可满足指派.上述算法不仅可以判定SAT问题,而且对于符合算法规定可满足的CNF公式皆可给出一个可满足指派.求解SAT问题的线性半定规划算法在文章中被描述并被给予相应算例.
关键词：SAT问题整数规划线性规划线性半定规划
分类号：TP301.6(计算技术、计算机技术)
资助基金：国家自然科学基金(60911130013)贵州省科学技术基金项目(2007]2003)
论文发表日期：2009-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：4( 4-6,78 )
英文信息