【摘 要】
:
该文描述了可满足性问题(SAT)求解器的设计及性能。首先,基于DPLL算法设计了一个单核SAT求解器的SystemC模型。校准这个模型,使之与工作站级计算机的软件性能相匹配,结果发现
【基金项目】
:
宁波市自然科学基金资助项目(2006A610009)
论文部分内容阅读
该文描述了可满足性问题(SAT)求解器的设计及性能。首先,基于DPLL算法设计了一个单核SAT求解器的SystemC模型。校准这个模型,使之与工作站级计算机的软件性能相匹配,结果发现通过不连续内存访问数可以准确地估计运行时间。接着,设计了一个多核SAT求解器模型,使之能共享学习短句。通过广泛地仿真,演示了这个方法的并行效率。针对DPLL算法并行化水平低时的性能退化问题,进行了算法改进,结果得到了明显的改善。
其他文献
研究水热合成氧化锌纳米棒的高温热稳定性。采用X射线衍射和扫描电镜对氧化锌纳米棒的结构与形貌进行表征。采用热重分析研究氧化锌纳米棒在热处理过程中的失重情况。结果表
在硫代硫酸盐浸出液中人工加入砷黄铁矿以了解砷黄铁矿在硫代硫酸盐浸金过程中发挥的作用。通过热力学计算、矿物溶解行为实验、浸出实验和XPS分析,研究砷黄铁矿对硫代硫酸盐
通过共沉淀法制备ZnO/ZnAl2O4纳米异质结光催化剂,利用HRTEM、TEM、XRD、BET、TG-DTA和UV-Vis DRS 测试方法对样品进行表征。在模拟太阳光照射下,通过测定甲基橙溶液的光催化降