【摘 要】
：
近10年来,布尔可满足性（SAT）求解技术飞速发展,并已经成功应用于模型检验、定理证明等领域,特别是在限界模型检验（BMC）中取得了明显的进展,然而,由于命题逻辑公式的长度随系统规
【机 构】
：
国防科学技术大学计算机学院,北京航空航天大学计算机学院
【基金项目】
：
国家自然科学基金项目（90718017 60703075）, 高等学校博士学科点专项科研基金项目（20070006055）
论文部分内容阅读
近10年来,布尔可满足性（SAT）求解技术飞速发展,并已经成功应用于模型检验、定理证明等领域,特别是在限界模型检验（BMC）中取得了明显的进展,然而,由于命题逻辑公式的长度随系统规模指数倍增长,基于SAT的模型检验仍然存在状态空间爆炸问题.带量词的布尔公式（QBF）作为SAT公式的自然扩展,具有紧凑的空间结构、更强大、更直观的表达能力,能够简洁地描述模型检验中的公式.基于QBF的模型检验有希望缓解状态空间爆炸问题,成为当前研究的一个热点.总结了当前主流的QBF求解算法及常用的优化技术,指出了该领域中值得关
其他文献
隐私保护是数据挖掘领域中一个极其重要而富有挑战性的课题，以实现隐私数据的保护和准确知识的挖掘两者兼得为其最终目标．统计回归是数据挖掘的常用工具之一，而数据分布式存储情
和谐社会以人为本之理念,在当今社会已深入人心,而具体化则有许多途径.生老病死泽被后世为中国人之传统.每个中国人的心中都为亲情所缠绕,每个中国人都希望无论在生前还是身
针对成本约束有向无环图DAG（directed acyclic graph）表示的网格工作流完工时间最小化问题,提出两个基于优先级规则的迭代启发算法.算法利用并行活动特征定义正向分层和逆向分