《算法1 算法主程序Alg.1 Main procedure of our algorithm》

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

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

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

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

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

ECWSAT主算法伪代码见算法1，软件预处理按照一定的策略计算各变元初始指派为正的概率。主程序中，根据计算的概率给变元赋初值，此时若CNF公式满足，则求解完成，并返回变元当前赋值。否则，随机选择一个不可满足的子句，以启发式Heuristic（c）选择某一布尔变元，并翻转变元赋值（由1变为0或者0变为1），然后判定CNF公式是否满足，若满足，则求解完成，返回变元当前赋值；若不满足，重复上一步骤直至找到问题的解或者在规定的时间内找不到解。其中，Maxtries和Maxflips用于控制算法的最长执行时间，分别代表未找到解时算法重新开始搜索的次数和单次搜索中允许变元翻转的次数。