由一阶逻辑公式得到命题逻辑可满足性问题实例

摘要：

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

关键词：可满足性问题、一阶逻辑、命题逻辑

所属期刊栏目：16

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60125207

在线出版日期：2005-03-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：327-335