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

• 作者: 张健 黄拙
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 可满足性问题 一阶逻辑 命题逻辑
• 年，卷（期）: 2005,（3）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 327-335
• 页数: 9页
• 分类号: TP301
• 字数: 1705字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张健		5	162	5.0	5.0