一阶逻辑中约束求解的局部搜索法

Local Search Methods for Constraint Solving in First Order Logic

以一阶谓词逻辑为基础，讨论约束满足问题．着重研究一阶逻辑公式可满足性的局部搜索法，并与命题逻辑中的可满足性过程加以比较．以皇后问题和哈密顿回路问题为例，说明基于一阶逻辑的方法能处理较大的问题实例．

In this paper, the author discusses constraint satisfaction problems in the framework of first order logic. Local search methods for satisfying first order formulas are studied, and compared with satisfiability procedures in the propositional logic. Experimental results on the Queens problem and the Hamiltanian circuit problem show that the framework is suitable for dealing with quite large problem instances.