求解SAT问题的线性半定规划算法

• 作者: 万武族 李厚银 许道云
• 来源期刊: 计算机与数字工程
• 学科: 工学
• 关键词: SAT问题 整数规划 线性规划 线性半定规划
• 年，卷（期）: 2009,（11）
• 所属期刊栏目: 算法与分析
• 页码范围: 4-6,78
• 页数: 4页
• 分类号: TP301.6
• 字数: 2728字
• 语种: 中文
• DOI: 10.3969/j.issn.1672-9722.2009.11.002

摘要

将线性半定规划应用到SAT问题的求解过程中.首先将SAT实例转化为整数规划问题,然后松弛为线性规划模型,最后再转化为一般的线性半定规划模型去求解.用SDPA-M软件求解线性半定规划问题后,规定了如何根据目标函数值去判定SAT实例和当CNF公式可满足时如何根据最优指派的概率x*i(i=1,…,n)去进行变元赋值,以期求得该公式的可满足指派.上述算法不仅可以判定SAT问题,而且对于符合算法规定可满足的CNF公式皆可给出一个可满足指派.求解SAT问题的线性半定规划算法在文章中被描述并被给予相应算例.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	许道云	贵州大学计算机科学系	125	460	12.0	16.0
2	万武族	贵州大学计算机科学系	3	22	2.0	3.0
3	李厚银	贵州大学理学院数学系	1	1	1.0	1.0