| 摘要: |
| 以一阶谓词逻辑为基础,讨论约束满足问题.着重研究一阶逻辑公式可满足性的局部搜索法,并与命题逻辑中的可满足性过程加以比较.以皇后问题和哈密顿回路问题为例,说明基于一阶逻辑的方法能处理较大的问题实例. |
| 关键词: 约束满足问题,一阶谓词逻辑,局部搜索. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家863高科技项目基金和中国科学院择优支持回国工作基金资助. |
|
| Local Search Methods for Constraint Solving in First-Order Logic |
|
ZHANG Jian
|
| Abstract: |
| 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. |
| Key words: Constraint satisfaction problems, first-order predicate logic, local search. |
