可满足性问题研究

数理逻辑是计算机科学的基础，而逻辑公式的可满足性问题是计算机科学和人工智能领域中的一个著名而又重要的问题。它在计算机科学和人工智能研究中有广泛的应用。本文将重点介绍实际可用的判定算法及其相关技术。 本文的研究分两大方向，分别是命题逻辑的可满足性问题研究和一阶逻辑的可满足性问题研究。命题逻辑的可满足性问题（Satisfiability Problem）是一个历史悠久的问题，一般简称为 SAT问题。SAT 问题的求解算法有两大类，分别是确定性算法和非确定性算法。本文只研究确定性算法的相关内容，尤其是如何进行剪枝。我们充分调研了SAT求解算法和求解工具的相关知识，在此基础上，提出了local Lemma 这个剪枝技术，该技术可以更加充分地挖掘剪枝信息，达到进行更多剪枝的目的。 在一阶逻辑的可满足性问题研究方面，本文采取直接搜索可行的一阶逻辑模型的方法研究有限论域上的一阶逻辑的可满足性问题。该方法本质上就是深度优先的回溯搜索。因此，我们的研究重点就是如何找到问题的更高效的一阶逻辑的表示以及如何采用启发式的方式进行剪枝。在这个问题上，我的主要工作有两个：一个是模型搜索中适用于谓词的同构消去技术，包括Row by Row策略和Ramsey Number 策略两个技术；另一个是 DASH（Decision Assignment Scheme Heuristic），用来在生成有限模型的时候边搜索边消除同构子空间。DASH 能用近乎零代价保证输出的模型都是互不同构的。这两个技术都是基于有限论域中的元素的固有对称性，换言之，就是需要有限论域中的元素是两两可交换的。 在已有的成果的基础上，我们又尝试使用它们去求解一些数学中的实际问题，如拟群拉丁方，有限射影平面，正交拉丁方（组）等。我们给出了在这几个方面的一些尝试和初步结果，包括一个重要的定理和若干效率提高了几个数量级的改进。 值得一提的是，和马菲菲共同提出的横截矩阵（Transversal Matrix）概念是一个新颖的成果，使得正交拉丁方的表示和求解取得了明显的改进。在这个概念的基础上，进一步给出了几个定理，进行了理论上的拓展。实验数据表明，我们的求解途径和技术能有效解决拉丁方相关的问题。