基于SystemC的SAT求解器设计

摘要：

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

关键词：可满足性问题、求解器、SystemC、DPLL

所属期刊栏目：6

分类号：TN915

资助基金：宁波市自然科学基金资助项目2006A610009

在线出版日期：2010-08-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共2页

页码：3774-3775