论文部分内容阅读
可满足性问题（SAT问题）是第一个被证明的NP完全问题，是当代理论计算机科学的核心问题。其快速求解算法不仅具有重要的理论意义，也具有重要的实际意义。可满足性问题求解算法在生产生活中的各个领域，如人工智能、计算机辅助设计、电路设计的形式化验证等都被广泛运用。因此，设计并实现求解SAT问题的高效算法意义重大。目前，高效的SAT求解算法主要分为完备算法和不完备算法两类。完备算法主要基于分支回溯策略，典型的有1962年由Martin Davis，Hilary Putnam，George Logemann和Donald W. Loveland提出的DPLL算法，后来的的大多数完备算法基本上都是在DPLL算法上提出新的化简规则和细化分支以提高效率，但算法的时间复杂度最差情况下还是指数级别的。不完备算法主要是基于随机搜索策略的局部搜索算法。虽然两种算法都在近些年的发展中取得了很大的进步，但都存在着不足，前者效率较低，后者不一定能找到对应SAT问题的解。本文提出了一种求解SAT问题的新思路，将求解SAT问题转化为线性代数问题，再运用单纯形法求解SAT问题的模型。本文的研究工作主要包括：（i）将可满足性问题的子句集转化为矩阵，通过对矩阵的变换，发现并证明了子句集系数矩阵的变化与可满足性问题的内在联系。通过找到合适的系数矩阵，就可以求解出一个子句集的可满足的赋值。（ii）在找到一个SAT问题合适的系数矩阵以后，基于单纯形法的的思想，实现一个SAT问题求解器。并选取SAT Competion给出的实验用例进行测试，用常归的MiniSat求解器进行测试结果验证，分析了影响求解器效率的因素。本文研究并设计了基于线性代数的SAT求解器，验证了正确性，展现了线性规划求解SAT问题的的能力，为研究SAT问题提供了新思路。