《表1 Walk SAT与ECWSAT性能比较Tab.1 Performance comparison between Walk SAT and ECWSAT》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《加强约束的布尔可满足硬件求解器》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

性能评估结果基于Xilinx Virtex-6 FPGA（xc6vhx565t）开发板，能处理多达32 000个变元/128 000个子句的实例，占用4%的slice和81%的片上RAM/FIFO，并通过求解不同规模的随机SAT实例对其性能进行测试。表1和表2将本文求解器分别与目前最新的软件求解器（WalkSAT Version 51[14]）和另一款硬件求解器[15]的性能做了比较。随机选择三个不同规模的测试用例，前两个来源于SATLIB Benchmark Problems[16]，后一个来源于SAT Competition[17]。WALKSAT Version51算法在Intel（R）Core（TM）i5 32-bit 2.3 GHz CPU 4.0 GB RAM Linux Ubuntu-14.04环境下编译，Maxflips取值30 000 000。依据SAT竞赛中的测试标准，每个测试实例测100次，取100次测试中成功测试的平均运行时间和变元翻转次数作为记录结果。表中，Nc、Nv和m分别表示子句数量、变元数量和子句长度，#flip为找到解时需要翻转的总步数，#fpsavg表示平均翻转速率，t为求解器找到解所需的执行时间。