由一阶逻辑公式得到命题逻辑可满足性问题实例
Data(s) |
2005
|
---|---|
Resumo |
命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为 SAT 问题.为了利用现有的高效 SAT工具,提出了一种从一阶逻辑公式生成 SAT 问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题. |
Identificador | |
Idioma(s) |
英语 |
Fonte |
黄拙; 张健.由一阶逻辑公式得到命题逻辑可满足性问题实例,软件学报,2005,16(3):327-335 |
Palavras-Chave | #可满足性问题 #一阶逻辑 #命题逻辑 #satisfiabilityproblem #first-orderlogic #propositionallogic |
Tipo |
期刊论文 |