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

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

Linear Semidefinite Programming Algorithm for SAT Problem

In this paper, SAT problem is solved by linear semidefinite programming algorithm. At first the SAT instances are translated into integer programming questions, then are slacked as linear programming model, at last they are solved by linear semidefinite programming method. After corresponding linear semidefinite programming questions are solved by SDPA-M, SAT instances can be judged by gotten objective values, and when CNF formulas are satisfiable, variables can be assigned by gotten probability values X^＊i（i=1,…,n）, so that the satisfiable assignmentes of these formulas can be got. By this algorithm, not only SAT problem can be judged, but the CNF formulas that are satisfiable and fit in with the algorithm rules can get corresponding satisfiable assignmentes. In this paper, linear semidefinite programming algorithm for SAT problem is described and the corresponding samples are provided.