论文部分内容阅读
非布尔变量的约束可满足性问题有两种较为普遍的求解方法 ,系统求解算法就是其中的一种。该算法的基本思想是对变量的值域空间逐个进行搜索 ,其优点是只要问题有解 ,算法就一定能给出正确答案。在最不理想的情况下 ,该算法时间复杂度为变量数目的指数级。该文给出一种新策略 ,虽然在本质上仍然是在值域空间中进行搜索 ,但在实现过程中根据启发式思想 ,有针对性地设置搜索的优先次序。它的目的是尽可能的缩小搜索空间的范围 ,因为实践证明算法计算过程中许多状态不需要搜索。几个实例证明该策略在许多情况下有较为令人满意的性能