中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
一阶逻辑模型搜索问题研究
作者: 黄拙
答辩日期: 2004
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 可满足性问题 ; 一阶逻辑 ; 命题逻辑 ; 有限模型
摘要: 命题逻辑可满足性(SAT)问题和有限论域一阶逻辑模型搜索(FOLMS)问题是计算机理论科学中的经典问题,不仅在理论上有着重要的地位,而且在许多实际问题中得到了广一泛的应用。多年来,学者们针对SAT问题进行了大量的研究,得到了许多有效的算法和工具;而FOLMS问题的研究虽然取得了一定的成果,但仍然显得较为薄弱。本文的工作是将这两个问题结合起来考虑,利用SAT问题的研究成果,结合FOLMS问题本身的特点,来改进FOLMS算法和工具。为了利用现有的高效SAT工具,研究了如何将FOLMS问题转换为sAT问题来求解,提出了一个新的转换算法,它能更好的利用SAT工具同时在转换效率上也有所提高。另一项研究工作是关于如何在转换法中利用FOLMS问题所具有的同构现象,通过添加约束从而减少转换所得的SAT问题的搜索空间。实验表明,这样的算法和约束是有效的,可以用来解决数学研究和实际应用中的许多问题。基于上述的算法,实现了一个实用的自动转换工具SAGE。为了提高FOLMS本身搜索算法的效率,研究了如何借鉴SAT问题算法现有研究成果来改进搜索算法。提出了一个新的直接搜索算法,它使用了在SAT问题中行之有效的冲突分析和学习机制。在具体实现该算法时,考虑了使用内嵌命题逻辑公式集和SAT工具来提高其实用性和效率。基于上述的算法和原有的FOLMS直接搜索工具SEM,实现了SEMLL工具。
英文摘要: 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.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6322
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW014066.pdf(2721KB)----限制开放-- 联系获取全文

Recommended Citation:
黄拙. 一阶逻辑模型搜索问题研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[黄拙]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[黄拙]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace