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

作者：宋富; 高鹏飞; 谢弘毅

来源：2020-09-02, 中国, ZL202010908484.5.

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

• 单位
  上海科技大学