| Title: | 一阶逻辑模型搜索问题研究 |
| Author: | 黄拙
|
| Issued Date: | 2004
|
| Major: | 计算机软件与理论
|
| Degree Grantor: | 中国科学院软件研究所
|
| Place of Degree Grantor: | 中国科学院软件研究所
|
| Degree Level: | 博士
|
| Keyword: | 可满足性问题
; 一阶逻辑
; 命题逻辑
; 有限模型
|
| Abstract: | 命题逻辑可满足性（SAT）问题和有限论域一阶逻辑模型搜索（FOLMS）问题是计算机理论科学中的经典问题，不仅在理论上有着重要的地位，而且在许多实际问题中得到了广一泛的应用。多年来，学者们针对SAT问题进行了大量的研究，得到了许多有效的算法和工具；而FOLMS问题的研究虽然取得了一定的成果，但仍然显得较为薄弱。本文的工作是将这两个问题结合起来考虑，利用SAT问题的研究成果，结合FOLMS问题本身的特点，来改进FOLMS算法和工具。为了利用现有的高效SAT工具，研究了如何将FOLMS问题转换为sAT问题来求解，提出了一个新的转换算法，它能更好的利用SAT工具同时在转换效率上也有所提高。另一项研究工作是关于如何在转换法中利用FOLMS问题所具有的同构现象，通过添加约束从而减少转换所得的SAT问题的搜索空间。实验表明，这样的算法和约束是有效的，可以用来解决数学研究和实际应用中的许多问题。基于上述的算法，实现了一个实用的自动转换工具SAGE。为了提高FOLMS本身搜索算法的效率，研究了如何借鉴SAT问题算法现有研究成果来改进搜索算法。提出了一个新的直接搜索算法，它使用了在SAT问题中行之有效的冲突分析和学习机制。在具体实现该算法时，考虑了使用内嵌命题逻辑公式集和SAT工具来提高其实用性和效率。基于上述的算法和原有的FOLMS直接搜索工具SEM，实现了SEMLL工具。 |
| English Abstract: | The algorithms and tools to solve first-order logic model searching (FOLMS) problem with finite domain size are studied in this thesis. The satisfiability(SAT) problem in the propositional logic and FOLMS are classic problems of computer science, which are important in theory and have wide applications in a lot of real-world problems. SAT has been throughly researched in recent years, and many algorithms and tools have been developed. In comparison with SAT, the algorithms and tools of FOLMS seem inefficient, although some progress has been made in this field. This thesis focuses on how to utilize the results of SAT research in FOLMS. A new algorithm to reduce the FOLMS to SAT is presented. Its can utilize the efficient SAT solvers more conveniently and the efficiency of conversion is improved. How to reduce the search space by adding constraints for eliminating symmetries is also discussed. The experiments show the effectiveness of the new algorithm and the constraints added. An automatic tool based on this algorithm is also described. A new FOLMS algorithm improved by lemma learning is presented. Lemma learning is an important technique of SAT research. For efficient reasons, the lemmas are represented in propositional formulas and a SAT solver is used to perform the necessary reasoning. Based on this algorithm, a new first-order model generator called SEMLL is developed, as the extension of the first-order model generator SEM. |
| Language: | 中文
|
| Content Type: | 学位论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/6322
|
| Appears in Collections: | 中科院软件所
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| LW014066.pdf（2721KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
黄拙. 一阶逻辑模型搜索问题研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004-01-01.
|
|
|
