基于SystemC的SAT求解器设计

摘要

该文描述了可满足性问题(SAT)求解器的设计及性能,首先,基于DPLL算法设计了一个单核SAT求解器的SystemC 模型.校准这个模型.使之与工作站级计算机的软件性能相匹配,结果发现通过不连续内存访问数可以准确地估计运行时间.接着,设计了一个多核SAT求解器模型,使之能共享学习短句.通过广泛地仿真,演示了这个方法的并行效率.针对DPLL算法并行化水平低时的性能退化问题,进行了算法改进,结果得到了明显的改善.