可满足性问题的约束求解器应用浅析

作     者：付江龙 杨阳 陈素军 赵天骄 FU Jiang-long;YANG Yang;CHEN Su-jun;ZHAO Tian-jiao

作者机构：河北建筑工程学院河北张家口075000 河北科技大学河北石家庄050000 

基　　金：2013年河北省教育厅青年基金项目(QN20131148) 河北省科技计划项目(16236004D-8) 

出 版 物：《河北建筑工程学院学报》 (Journal of Hebei Institute of Architecture and Civil Engineering)

年 卷 期：2017年第35卷第2期

页      码：132-134页

摘      要：约束求解问题涉及广泛,解决约束求解问题的一个重要方法就是SMT理论.本文介绍了两种利用SMT理论设计的约束求解器,分析了其求解原理和主要应用,并对以上两种约束求解器的优缺点进行探讨.约束求解器的研究为解决相对应的约束求解问题提供了思路和方法.

主 题 词：约束求解 YICES HySat 

学科分类：08[工学] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1008-4185.2017.02.032

馆 藏 号：203237129...