一阶逻辑模型搜索问题研究
文献类型：学位论文
| 作者 | 黄拙 |
| 学位类别 | 博士 |
| 答辩日期 | 2004 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 可满足性问题 一阶逻辑 命题逻辑 有限模型 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 命题逻辑可满足性（SAT）问题和有限论域一阶逻辑模型搜索（FOLMS）问题是计算机理论科学中的经典问题，不仅在理论上有着重要的地位，而且在许多实际问题中得到了广一泛的应用。多年来，学者们针对SAT问题进行了大量的研究，得到了许多有效的算法和工具；而FOLMS问题的研究虽然取得了一定的成果，但仍然显得较为薄弱。本文的工作是将这两个问题结合起来考虑，利用SAT问题的研究成果，结合FOLMS问题本身的特点，来改进FOLMS算法和工具。为了利用现有的高效SAT工具，研究了如何将FOLMS问题转换为sAT问题来求解，提出了一个新的转换算法，它能更好的利用SAT工具同时在转换效率上也有所提高。另一项研究工作是关于如何在转换法中利用FOLMS问题所具有的同构现象，通过添加约束从而减少转换所得的SAT问题的搜索空间。实验表明，这样的算法和约束是有效的，可以用来解决数学研究和实际应用中的许多问题。基于上述的算法，实现了一个实用的自动转换工具SAGE。为了提高FOLMS本身搜索算法的效率，研究了如何借鉴SAT问题算法现有研究成果来改进搜索算法。提出了一个新的直接搜索算法，它使用了在SAT问题中行之有效的冲突分析和学习机制。在具体实现该算法时，考虑了使用内嵌命题逻辑公式集和SAT工具来提高其实用性和效率。基于上述的算法和原有的FOLMS直接搜索工具SEM，实现了SEMLL工具。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 83 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6322]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 黄拙. 一阶逻辑模型搜索问题研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。