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


Autoria(s): 黄拙; 张健
Data(s)

2005

Resumo

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

Identificador

http://ir.iscas.ac.cn/handle/311060/3128

http://www.irgrid.ac.cn/handle/1471x/66684

Idioma(s)

英语

Fonte

黄拙; 张健.由一阶逻辑公式得到命题逻辑可满足性问题实例,软件学报,2005,16(3):327-335

Palavras-Chave #可满足性问题 #一阶逻辑 #命题逻辑 #satisfiabilityproblem #first-orderlogic #propositionallogic
Tipo

期刊论文