一种基于GPU的模型计数及其约束的求解方法

摘要

本发明涉及一种基于GPU的模型计数及其约束的求解方法，其特征在于，包括以下步骤：利用编译技术将逻辑公式及其约束翻译到中间表示形式；根据GPU信息和逻辑公式，将程序变量划分为三个集合分别用CPU、GPU线程标识符和GPU枚举具体取值；生成GPU源代码程序并编译执行，GPU程序执行结果为逻辑公式及其约束的求解结果。本发明达到了显著的性能提升效果。通过多个实验，本发明达到了显著的性能提升效果，本发明提出的方法比传统基于CPU枚举的和SMT求解器的方法相比，性能提升数百倍。