文件名称：ParaFROST:具有GPU加速处理功能的SAT解算器
文件大小：248KB
文件格式：ZIP
更新时间：2024-04-27 11:03:34
C++
ParaFrost ParaFROST表示可满足性的并行形式推理。 它是具有GPU加速处理能力的并行SAT求解器，能够利用NIVIDA CUDA支持的GPU并行应用现代处理技术。 CDCL搜索是基于CaDiCaL启发式算法从头开始构建的，并进行了各种优化（请参见中的）。 数据处理引擎通过新的数据结构，并行垃圾收集等功能扩展了我们先前在SIGmA简化器中的工作。 安装 运行make -C gpu生成gpu求解器，或运行make -C cpu生成仅CPU的版本。 在make命令中添加assert=1参数以启用断言，或者debug=1收集CPU和GPU求解器的调试信息。 默认情况下，将在求解器本地目录中创建parafrost二进制文件和库libparafrost.a 。 在运行GPU求解器之前，请确保您具有支持CUDA的GPU。 该求解器具有用于评估和与CaDiCaL求解器进行比较的完整工件